A4: for A being non-empty MSAlgebra of 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 of 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:12;
A7: for A, B being non-empty MSAlgebra of F1() st A,B are_isomorphic & P1[A] holds
P1[B] by A1;
consider A being strict non-empty MSAlgebra of 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 of 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 of 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 of 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 of 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 of 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 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 F2())) = GG || (FreeGen F2()) by A15, EXTENS_1:8;
A17: F is "onto" by A9, MSUALG_3:def 10;
rngs (Reverse F2()) = F2() by EXTENS_1:14;
then A18: Reverse F2() is "onto" by EXTENS_1:13;
R ** (Reverse F2()) = (F || (FreeGen F2())) ** (((Reverse F2()) "") ** (Reverse F2())) by PBOOLE:154
.= (F || (FreeGen F2())) ** (id (FreeGen F2())) by A18, A6, MSUALG_3:5
.= F || (FreeGen F2()) by MSUALG_3:3 ;
then A19: (H ** R) ** (Reverse F2()) = G ** (Reverse F2()) by A13, A16, PBOOLE:154;
hence H ** R = G by A18, EXTENS_1:16; :: 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 A19, PBOOLE:154;
then K ** (((F || (FreeGen F2())) ** ((Reverse F2()) "")) ** (Reverse F2())) = H ** (((F || (FreeGen F2())) ** ((Reverse F2()) "")) ** (Reverse F2())) by PBOOLE:154;
then K ** ((F || (FreeGen F2())) ** (((Reverse F2()) "") ** (Reverse F2()))) = H ** (((F || (FreeGen F2())) ** ((Reverse F2()) "")) ** (Reverse F2())) by PBOOLE:154;
then K ** ((F || (FreeGen F2())) ** (((Reverse F2()) "") ** (Reverse F2()))) = H ** ((F || (FreeGen F2())) ** (((Reverse F2()) "") ** (Reverse F2()))) by PBOOLE:154;
then K ** ((F || (FreeGen F2())) ** (id (FreeGen F2()))) = H ** ((F || (FreeGen F2())) ** (((Reverse F2()) "") ** (Reverse F2()))) by A18, A6, MSUALG_3:5;
then K ** ((F || (FreeGen F2())) ** (id (FreeGen F2()))) = H ** ((F || (FreeGen F2())) ** (id (FreeGen F2()))) by A18, A6, MSUALG_3:5;
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:8;
then A21: (K ** F) || (FreeGen F2()) = (H ** F) || (FreeGen F2()) by EXTENS_1:8;
F is_homomorphism FreeMSA F2(),A by A9, MSUALG_3:def 10;
then K ** F is_homomorphism FreeMSA F2(),B by A20, MSUALG_3:10;
then K ** F = H ** F by A12, A15, A21, EXTENS_1:18;
hence H = K by A17, EXTENS_1:16; :: thesis: verum