A4:
for A being non-empty MSAlgebra over F_{1}()

for B being strict non-empty MSSubAlgebra of A st P_{1}[A] holds

P_{1}[B]
by A2;

A5: for I being set

for F being MSAlgebra-Family of I,F_{1}() st ( for i being set st i in I holds

ex A being MSAlgebra over F_{1}() st

( A = F . i & P_{1}[A] ) ) holds

P_{1}[ product F]
by A3;

set FM = FreeMSA F_{2}();

A6: Reverse F_{2}() is "1-1"
by MSUALG_9:11;

A7: for A, B being non-empty MSAlgebra over F_{1}() st A,B are_isomorphic & P_{1}[A] holds

P_{1}[B]
by A1;

consider A being strict non-empty MSAlgebra over F_{1}(), F being ManySortedFunction of (FreeMSA F_{2}()),A such that

A8: P_{1}[A]
and

A9: F is_epimorphism FreeMSA F_{2}(),A
and

A10: for B being non-empty MSAlgebra over F_{1}()

for G being ManySortedFunction of (FreeMSA F_{2}()),B st G is_homomorphism FreeMSA F_{2}(),B & P_{1}[B] holds

ex H being ManySortedFunction of A,B st

( H is_homomorphism A,B & H ** F = G & ( for K being ManySortedFunction of A,B st K ** F = G holds

H = K ) ) from BIRKHOFF:sch 1(A7, A4, A5);

reconsider R = (F || (FreeGen F_{2}())) ** ((Reverse F_{2}()) "") as ManySortedFunction of F_{2}(), the Sorts of A ;

take A ; :: thesis: ex F being ManySortedFunction of F_{2}(), the Sorts of A st

( P_{1}[A] & ( for B being non-empty MSAlgebra over F_{1}()

for G being ManySortedFunction of F_{2}(), the Sorts of B st P_{1}[B] holds

ex H being ManySortedFunction of A,B st

( H is_homomorphism A,B & H ** F = G & ( for K being ManySortedFunction of A,B st K is_homomorphism A,B & K ** F = G holds

H = K ) ) ) )

take R ; :: thesis: ( P_{1}[A] & ( for B being non-empty MSAlgebra over F_{1}()

for G being ManySortedFunction of F_{2}(), the Sorts of B st P_{1}[B] holds

ex H being ManySortedFunction of A,B st

( H is_homomorphism A,B & H ** R = G & ( for K being ManySortedFunction of A,B st K is_homomorphism A,B & K ** R = G holds

H = K ) ) ) )

thus P_{1}[A]
by A8; :: thesis: for B being non-empty MSAlgebra over F_{1}()

for G being ManySortedFunction of F_{2}(), the Sorts of B st P_{1}[B] holds

ex H being ManySortedFunction of A,B st

( H is_homomorphism A,B & H ** R = G & ( for K being ManySortedFunction of A,B st K is_homomorphism A,B & K ** R = G holds

H = K ) )

let B be non-empty MSAlgebra over F_{1}(); :: thesis: for G being ManySortedFunction of F_{2}(), the Sorts of B st P_{1}[B] holds

ex H being ManySortedFunction of A,B st

( H is_homomorphism A,B & H ** R = G & ( for K being ManySortedFunction of A,B st K is_homomorphism A,B & K ** R = G holds

H = K ) )

let G be ManySortedFunction of F_{2}(), the Sorts of B; :: thesis: ( P_{1}[B] implies ex H being ManySortedFunction of A,B st

( H is_homomorphism A,B & H ** R = G & ( for K being ManySortedFunction of A,B st K is_homomorphism A,B & K ** R = G holds

H = K ) ) )

assume A11: P_{1}[B]
; :: thesis: ex H being ManySortedFunction of A,B st

( H is_homomorphism A,B & H ** R = G & ( for K being ManySortedFunction of A,B st K is_homomorphism A,B & K ** R = G holds

H = K ) )

consider GG being ManySortedFunction of (FreeMSA F_{2}()),B such that

A12: GG is_homomorphism FreeMSA F_{2}(),B
and

A13: GG || (FreeGen F_{2}()) = G ** (Reverse F_{2}())
by MSAFREE:def 5;

consider H being ManySortedFunction of A,B such that

A14: H is_homomorphism A,B and

A15: H ** F = GG and

for K being ManySortedFunction of A,B st K ** F = GG holds

H = K by A10, A11, A12;

take H ; :: thesis: ( H is_homomorphism A,B & H ** R = G & ( for K being ManySortedFunction of A,B st K is_homomorphism A,B & K ** R = G holds

H = K ) )

thus H is_homomorphism A,B by A14; :: thesis: ( H ** R = G & ( for K being ManySortedFunction of A,B st K is_homomorphism A,B & K ** R = G holds

H = K ) )

A16: H ** (F || (FreeGen F_{2}())) = GG || (FreeGen F_{2}())
by A15, EXTENS_1:4;

A17: F is "onto" by A9, MSUALG_3:def 8;

rngs (Reverse F_{2}()) = F_{2}()
by EXTENS_1:10;

then A18: Reverse F_{2}() is "onto"
by EXTENS_1:9;

R ** (Reverse F_{2}()) =
(F || (FreeGen F_{2}())) ** (((Reverse F_{2}()) "") ** (Reverse F_{2}()))
by PBOOLE:140

.= (F || (FreeGen F_{2}())) ** (id (FreeGen F_{2}()))
by A18, A6, MSUALG_3:5

.= F || (FreeGen F_{2}())
by MSUALG_3:3
;

then A19: (H ** R) ** (Reverse F_{2}()) = G ** (Reverse F_{2}())
by A13, A16, PBOOLE:140;

hence H ** R = G by A18, EXTENS_1:12; :: thesis: for K being ManySortedFunction of A,B st K is_homomorphism A,B & K ** R = G holds

H = K

let K be ManySortedFunction of A,B; :: thesis: ( K is_homomorphism A,B & K ** R = G implies H = K )

assume A20: K is_homomorphism A,B ; :: thesis: ( not K ** R = G or H = K )

assume K ** R = G ; :: thesis: H = K

then K ** (((F || (FreeGen F_{2}())) ** ((Reverse F_{2}()) "")) ** (Reverse F_{2}())) = (H ** ((F || (FreeGen F_{2}())) ** ((Reverse F_{2}()) ""))) ** (Reverse F_{2}())
by A19, PBOOLE:140;

then K ** (((F || (FreeGen F_{2}())) ** ((Reverse F_{2}()) "")) ** (Reverse F_{2}())) = H ** (((F || (FreeGen F_{2}())) ** ((Reverse F_{2}()) "")) ** (Reverse F_{2}()))
by PBOOLE:140;

then K ** ((F || (FreeGen F_{2}())) ** (((Reverse F_{2}()) "") ** (Reverse F_{2}()))) = H ** (((F || (FreeGen F_{2}())) ** ((Reverse F_{2}()) "")) ** (Reverse F_{2}()))
by PBOOLE:140;

then K ** ((F || (FreeGen F_{2}())) ** (((Reverse F_{2}()) "") ** (Reverse F_{2}()))) = H ** ((F || (FreeGen F_{2}())) ** (((Reverse F_{2}()) "") ** (Reverse F_{2}())))
by PBOOLE:140;

then K ** ((F || (FreeGen F_{2}())) ** (id (FreeGen F_{2}()))) = H ** ((F || (FreeGen F_{2}())) ** (((Reverse F_{2}()) "") ** (Reverse F_{2}())))
by A18, A6, MSUALG_3:5;

then K ** ((F || (FreeGen F_{2}())) ** (id (FreeGen F_{2}()))) = H ** ((F || (FreeGen F_{2}())) ** (id (FreeGen F_{2}())))
by A18, A6, MSUALG_3:5;

then K ** (F || (FreeGen F_{2}())) = H ** ((F || (FreeGen F_{2}())) ** (id (FreeGen F_{2}())))
by MSUALG_3:3;

then K ** (F || (FreeGen F_{2}())) = H ** (F || (FreeGen F_{2}()))
by MSUALG_3:3;

then (K ** F) || (FreeGen F_{2}()) = H ** (F || (FreeGen F_{2}()))
by EXTENS_1:4;

then A21: (K ** F) || (FreeGen F_{2}()) = (H ** F) || (FreeGen F_{2}())
by EXTENS_1:4;

F is_homomorphism FreeMSA F_{2}(),A
by A9, MSUALG_3:def 8;

then K ** F is_homomorphism FreeMSA F_{2}(),B
by A20, MSUALG_3:10;

then K ** F = H ** F by A12, A15, A21, EXTENS_1:14;

hence H = K by A17, EXTENS_1:12; :: thesis: verum

for B being strict non-empty MSSubAlgebra of A st P

P

A5: for I being set

for F being MSAlgebra-Family of I,F

ex A being MSAlgebra over F

( A = F . i & P

P

set FM = FreeMSA F

A6: Reverse F

A7: for A, B being non-empty MSAlgebra over F

P

consider A being strict non-empty MSAlgebra over F

A8: P

A9: F is_epimorphism FreeMSA F

A10: for B being non-empty MSAlgebra over F

for G being ManySortedFunction of (FreeMSA F

ex H being ManySortedFunction of A,B st

( H is_homomorphism A,B & H ** F = G & ( for K being ManySortedFunction of A,B st K ** F = G holds

H = K ) ) from BIRKHOFF:sch 1(A7, A4, A5);

reconsider R = (F || (FreeGen F

take A ; :: thesis: ex F being ManySortedFunction of F

( P

for G being ManySortedFunction of F

ex H being ManySortedFunction of A,B st

( H is_homomorphism A,B & H ** F = G & ( for K being ManySortedFunction of A,B st K is_homomorphism A,B & K ** F = G holds

H = K ) ) ) )

take R ; :: thesis: ( P

for G being ManySortedFunction of F

ex H being ManySortedFunction of A,B st

( H is_homomorphism A,B & H ** R = G & ( for K being ManySortedFunction of A,B st K is_homomorphism A,B & K ** R = G holds

H = K ) ) ) )

thus P

for G being ManySortedFunction of F

ex H being ManySortedFunction of A,B st

( H is_homomorphism A,B & H ** R = G & ( for K being ManySortedFunction of A,B st K is_homomorphism A,B & K ** R = G holds

H = K ) )

let B be non-empty MSAlgebra over F

ex H being ManySortedFunction of A,B st

( H is_homomorphism A,B & H ** R = G & ( for K being ManySortedFunction of A,B st K is_homomorphism A,B & K ** R = G holds

H = K ) )

let G be ManySortedFunction of F

( H is_homomorphism A,B & H ** R = G & ( for K being ManySortedFunction of A,B st K is_homomorphism A,B & K ** R = G holds

H = K ) ) )

assume A11: P

( H is_homomorphism A,B & H ** R = G & ( for K being ManySortedFunction of A,B st K is_homomorphism A,B & K ** R = G holds

H = K ) )

consider GG being ManySortedFunction of (FreeMSA F

A12: GG is_homomorphism FreeMSA F

A13: GG || (FreeGen F

consider H being ManySortedFunction of A,B such that

A14: H is_homomorphism A,B and

A15: H ** F = GG and

for K being ManySortedFunction of A,B st K ** F = GG holds

H = K by A10, A11, A12;

take H ; :: thesis: ( H is_homomorphism A,B & H ** R = G & ( for K being ManySortedFunction of A,B st K is_homomorphism A,B & K ** R = G holds

H = K ) )

thus H is_homomorphism A,B by A14; :: thesis: ( H ** R = G & ( for K being ManySortedFunction of A,B st K is_homomorphism A,B & K ** R = G holds

H = K ) )

A16: H ** (F || (FreeGen F

A17: F is "onto" by A9, MSUALG_3:def 8;

rngs (Reverse F

then A18: Reverse F

R ** (Reverse F

.= (F || (FreeGen F

.= F || (FreeGen F

then A19: (H ** R) ** (Reverse F

hence H ** R = G by A18, EXTENS_1:12; :: thesis: for K being ManySortedFunction of A,B st K is_homomorphism A,B & K ** R = G holds

H = K

let K be ManySortedFunction of A,B; :: thesis: ( K is_homomorphism A,B & K ** R = G implies H = K )

assume A20: K is_homomorphism A,B ; :: thesis: ( not K ** R = G or H = K )

assume K ** R = G ; :: thesis: H = K

then K ** (((F || (FreeGen F

then K ** (((F || (FreeGen F

then K ** ((F || (FreeGen F

then K ** ((F || (FreeGen F

then K ** ((F || (FreeGen F

then K ** ((F || (FreeGen F

then K ** (F || (FreeGen F

then K ** (F || (FreeGen F

then (K ** F) || (FreeGen F

then A21: (K ** F) || (FreeGen F

F is_homomorphism FreeMSA F

then K ** F is_homomorphism FreeMSA F

then K ** F = H ** F by A12, A15, A21, EXTENS_1:14;

hence H = K by A17, EXTENS_1:12; :: thesis: verum