A4: for A being non-empty MSAlgebra over F1()
for B being strict non-empty MSSubAlgebra of A st P1[A] holds
P1[B] by A2;
A5: for I being set
for F being MSAlgebra-Family of I,F1() st ( for i being set st i in I holds
ex A being MSAlgebra over F1() st
( A = F . i & P1[A] ) ) holds
P1[ product F] by A3;
set FM = FreeMSA F2();
A6: Reverse F2() is "1-1" by MSUALG_9:11;
A7: for A, B being non-empty MSAlgebra over F1() st A,B are_isomorphic & P1[A] holds
P1[B] by A1;
consider A being strict non-empty MSAlgebra over F1(), F being ManySortedFunction of (FreeMSA F2()),A such that
A8: P1[A] and
A9: F is_epimorphism FreeMSA F2(),A and
A10: for B being non-empty MSAlgebra over F1()
for G being ManySortedFunction of (FreeMSA F2()),B st G is_homomorphism FreeMSA F2(),B & P1[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 F2())) ** ((Reverse F2()) "") as ManySortedFunction of F2(), the Sorts of A ;
take A ; :: thesis: ex F being ManySortedFunction of F2(), the Sorts of A st
( P1[A] & ( for B being non-empty MSAlgebra over F1()
for G being ManySortedFunction of F2(), the Sorts of B st P1[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: ( P1[A] & ( for B being non-empty MSAlgebra over F1()
for G being ManySortedFunction of F2(), the Sorts of B st P1[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 P1[A] by A8; :: thesis: for B being non-empty MSAlgebra over F1()
for G being ManySortedFunction of F2(), the Sorts of B st P1[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 F1(); :: thesis: for G being ManySortedFunction of F2(), the Sorts of B st P1[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 F2(), the Sorts of B; :: thesis: ( P1[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: P1[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 F2()),B such that
A12: GG is_homomorphism FreeMSA F2(),B and
A13: GG || (FreeGen F2()) = G ** (Reverse F2()) 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 ;
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 F2())) = GG || (FreeGen F2()) by ;
A17: F is "onto" by ;
rngs (Reverse F2()) = F2() by EXTENS_1:10;
then A18: Reverse F2() is "onto" by EXTENS_1:9;
R ** (Reverse F2()) = (F || (FreeGen F2())) ** (((Reverse F2()) "") ** (Reverse F2())) by PBOOLE:140
.= (F || (FreeGen F2())) ** (id (FreeGen F2())) by
.= F || (FreeGen F2()) by MSUALG_3:3 ;
then A19: (H ** R) ** (Reverse F2()) = G ** (Reverse F2()) by ;
hence H ** R = G by ; :: 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 F2())) ** ((Reverse F2()) "")) ** (Reverse F2())) = (H ** ((F || (FreeGen F2())) ** ((Reverse F2()) ""))) ** (Reverse F2()) by ;
then K ** (((F || (FreeGen F2())) ** ((Reverse F2()) "")) ** (Reverse F2())) = H ** (((F || (FreeGen F2())) ** ((Reverse F2()) "")) ** (Reverse F2())) by PBOOLE:140;
then K ** ((F || (FreeGen F2())) ** (((Reverse F2()) "") ** (Reverse F2()))) = H ** (((F || (FreeGen F2())) ** ((Reverse F2()) "")) ** (Reverse F2())) by PBOOLE:140;
then K ** ((F || (FreeGen F2())) ** (((Reverse F2()) "") ** (Reverse F2()))) = H ** ((F || (FreeGen F2())) ** (((Reverse F2()) "") ** (Reverse F2()))) by PBOOLE:140;
then K ** ((F || (FreeGen F2())) ** (id (FreeGen F2()))) = H ** ((F || (FreeGen F2())) ** (((Reverse F2()) "") ** (Reverse F2()))) by ;
then K ** ((F || (FreeGen F2())) ** (id (FreeGen F2()))) = H ** ((F || (FreeGen F2())) ** (id (FreeGen F2()))) by ;
then K ** (F || (FreeGen F2())) = H ** ((F || (FreeGen F2())) ** (id (FreeGen F2()))) by MSUALG_3:3;
then K ** (F || (FreeGen F2())) = H ** (F || (FreeGen F2())) by MSUALG_3:3;
then (K ** F) || (FreeGen F2()) = H ** (F || (FreeGen F2())) by EXTENS_1:4;
then A21: (K ** F) || (FreeGen F2()) = (H ** F) || (FreeGen F2()) by EXTENS_1:4;
F is_homomorphism FreeMSA F2(),A by ;
then K ** F is_homomorphism FreeMSA F2(),B by ;
then K ** F = H ** F by ;
hence H = K by ; :: thesis: verum