Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Apply unknownprop_94c3be6982bd677952253aa29af894411b7bd1f90353a0d2fdecf3d31d757dbd with
x0,
λ x4 . MagmaHom x4 x1 x2 ⟶ MagmaHom x4 x1 x3 ⟶ Quasigroup (32592.. x4 x1 x2 x3) leaving 2 subgoals.
The subproof is completed by applying H1.
Let x4 of type ι be given.
Let x5 of type ι → ι → ι be given.
Assume H3: ∀ x6 . x6 ∈ x4 ⟶ ∀ x7 . x7 ∈ x4 ⟶ x5 x6 x7 ∈ x4.
Assume H4:
∀ x6 . x6 ∈ x4 ⟶ bij x4 x4 (x5 x6).
Assume H5:
∀ x6 . x6 ∈ x4 ⟶ bij x4 x4 (λ x7 . x5 x7 x6).
Apply unknownprop_94c3be6982bd677952253aa29af894411b7bd1f90353a0d2fdecf3d31d757dbd with
x1,
λ x6 . MagmaHom (pack_b x4 x5) x6 x2 ⟶ MagmaHom (pack_b x4 x5) x6 x3 ⟶ Quasigroup (32592.. (pack_b x4 x5) x6 x2 x3) leaving 2 subgoals.
The subproof is completed by applying H2.
Let x6 of type ι be given.
Let x7 of type ι → ι → ι be given.
Assume H6: ∀ x8 . x8 ∈ x6 ⟶ ∀ x9 . x9 ∈ x6 ⟶ x7 x8 x9 ∈ x6.
Assume H7:
∀ x8 . x8 ∈ x6 ⟶ bij x6 x6 (x7 x8).
Assume H8:
∀ x8 . x8 ∈ x6 ⟶ bij x6 x6 (λ x9 . x7 x9 x8).
Apply unknownprop_7ee20a9b005b9d1cb4acab7f037a1615344131a99780aaa35f8fa78a1fc7660f with
x4,
x6,
x5,
x7,
x2,
λ x8 x9 : ο . x9 ⟶ MagmaHom (pack_b x4 x5) (pack_b x6 x7) x3 ⟶ Quasigroup (32592.. (pack_b x4 x5) (pack_b x6 x7) x2 x3).
Apply unknownprop_7ee20a9b005b9d1cb4acab7f037a1615344131a99780aaa35f8fa78a1fc7660f with
x4,
x6,
x5,
x7,
x3,
λ x8 x9 : ο . and (x2 ∈ setexp x6 x4) (∀ x10 . x10 ∈ x4 ⟶ ∀ x11 . x11 ∈ x4 ⟶ ap x2 (x5 x10 x11) = x7 (ap x2 x10) (ap x2 x11)) ⟶ x9 ⟶ Quasigroup (32592.. (pack_b x4 x5) (pack_b x6 x7) x2 x3).
Assume H9:
and (x2 ∈ setexp x6 x4) (∀ x8 . x8 ∈ x4 ⟶ ∀ x9 . x9 ∈ x4 ⟶ ap x2 (x5 x8 x9) = x7 (ap x2 x8) (ap x2 x9)).
Apply unknownprop_e61ba9aff4fd349c1c42f2a34d877d749901dbe2942e4d83737a99cb0fa8568b with
Quasigroup leaving 2 subgoals.
The subproof is completed by applying L0.
The subproof is completed by applying L1.