consider M being strict feasible MSAlgebra over S such that
A3: i = M and
A4: for C being Component of the Sorts of M holds C c= A by A1, Def2;
consider N being strict feasible MSAlgebra over S such that
A5: j = N and
A6: for C being Component of the Sorts of N holds C c= A by A2, Def2;
defpred S₁[ object ] means ( the Sorts of M is_transformable_to the Sorts of N & ex f being ManySortedFunction of M,N st
( $1 = f & f is_homomorphism M,N ) );
consider X being set such that
A7: for x being object holds
( x in X iff ( x in Funcs ( the carrier of S,(PFuncs ((union (bool A)),(union (bool A))))) & S₁[x] ) ) from XBOOLE_0:sch 1();
take X ; :: thesis: for x being set holds
( x in X iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st
( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) )
let x be set ; :: thesis: ( x in X iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st
( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) )

hereby :: thesis: ( ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st
( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) implies x in X )

assume A8: x in X ; :: thesis: ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st
( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N )
then consider f being ManySortedFunction of M,N such that
A9: x = f and
A10: f is_homomorphism M,N by A7;
take M = M; :: thesis: ex N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st
( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N )
take N = N; :: thesis: ex f being ManySortedFunction of M,N st
( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N )
reconsider f = f as ManySortedFunction of M,N ;
take f = f; :: thesis: ( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N )
thus ( M = i & N = j & f = x ) by A3, A5, A9; :: thesis: ( the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N )
thus the Sorts of M is_transformable_to the Sorts of N by A8, A7; :: thesis: f is_homomorphism M,N
thus f is_homomorphism M,N by A10; :: thesis: verum

end;

given M1, N1 being strict feasible MSAlgebra over S, f being ManySortedFunction of M1,N1 such that A11: ( M1 = i & N1 = j & f = x & the Sorts of M1 is_transformable_to the Sorts of N1 & f is_homomorphism M1,N1 ) ; :: thesis: x in X
reconsider F = f as ManySortedFunction of M,N by A11, A3, A5;
A12: dom F = the carrier of S by PARTFUN1:def 2;
rng F c= PFuncs ((union (bool A)),(union (bool A)))

proof

A13: rng the Sorts of M c= bool A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng the Sorts of M or x in bool A )
assume x in rng the Sorts of M ; :: thesis: x in bool A
then reconsider x9 = x as Component of the Sorts of M ;
x9 c= A by A4;
hence x in bool A ; :: thesis: verum

end;

let w be object ; :: according to TARSKI:def 3 :: thesis: ( not w in rng F or w in PFuncs ((union (bool A)),(union (bool A))) )
assume w in rng F ; :: thesis: w in PFuncs ((union (bool A)),(union (bool A)))
then consider w1 being object such that
A14: w1 in dom F and
A15: w = F . w1 by FUNCT_1:def 3;
reconsider w9 = w as Function of ( the Sorts of M . w1),( the Sorts of N . w1) by A14, A15, PBOOLE:def 15;
A16: dom the Sorts of M = the carrier of S by PARTFUN1:def 2;
A17: dom w9 c= union (bool A)

proof

let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in dom w9 or s in union (bool A) )
assume A18: s in dom w9 ; :: thesis: s in union (bool A)
the Sorts of M . w1 in rng the Sorts of M by A14, A16, FUNCT_1:def 3;
hence s in union (bool A) by A13, A18, TARSKI:def 4; :: thesis: verum

end;

A19: rng the Sorts of N c= bool A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng the Sorts of N or x in bool A )
assume x in rng the Sorts of N ; :: thesis: x in bool A
then reconsider x9 = x as Component of the Sorts of N ;
x9 c= A by A6;
hence x in bool A ; :: thesis: verum

end;

A20: dom the Sorts of N = the carrier of S by PARTFUN1:def 2;
rng w9 c= union (bool A)

proof

let r be object ; :: according to TARSKI:def 3 :: thesis: ( not r in rng w9 or r in union (bool A) )
assume A21: r in rng w9 ; :: thesis: r in union (bool A)
the Sorts of N . w1 in rng the Sorts of N by A14, A20, FUNCT_1:def 3;
hence r in union (bool A) by A19, A21, TARSKI:def 4; :: thesis: verum

end;

hence w in PFuncs ((union (bool A)),(union (bool A))) by A17, PARTFUN1:def 3; :: thesis: verum

end;

then F in Funcs ( the carrier of S,(PFuncs ((union (bool A)),(union (bool A))))) by A12, FUNCT_2:def 2;
hence x in X by A7, A11, A3, A5; :: thesis: verum