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_{1}[ 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_{1}[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 ) )

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)))

hence x in X by A7, A11, A3, A5; :: thesis: verum

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

( $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

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 )

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( 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;( 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

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

then
F in Funcs ( the carrier of S,(PFuncs ((union (bool A)),(union (bool A)))))
by A12, FUNCT_2:def 2;
A13:
rng the Sorts of M c= 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)

rng w9 c= union (bool A)

end;proof

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))) )
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;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

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

A19:
rng the Sorts of N c= bool A
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;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

proof

A20:
dom the Sorts of N = the carrier of S
by PARTFUN1:def 2;
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;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

rng w9 c= union (bool A)

proof

hence
w in PFuncs ((union (bool A)),(union (bool A)))
by A17, PARTFUN1:def 3; :: thesis: verum
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;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

hence x in X by A7, A11, A3, A5; :: thesis: verum