defpred S₁[ set , set ] means ex M, N being strict feasible MSAlgebra of S ex F being ManySortedFunction of M,N st
( $2 = F & i = M & j = N & $1 = [ the Sorts of M, the Charact of M, the Sorts of N, the Charact of N,F] & the Sorts of M is_transformable_to the Sorts of N & F is_homomorphism M,N );
A3: for x, y, z being set st S₁[x,y] & S₁[x,z] holds
y = z by MCART_2:6;
consider X being set such that
A4: for x being set holds
( x in X iff ex y being set st
( y in [:(Funcs ( the carrier of S,(bool A))),(Funcs ( the carrier' of S,(PFuncs ((PFuncs (NAT,A)),A)))),(Funcs ( the carrier of S,(bool A))),(Funcs ( the carrier' of S,(PFuncs ((PFuncs (NAT,A)),A)))),(Funcs ( the carrier of S,(PFuncs ((union (bool A)),(union (bool A)))))):] & S₁[y,x] ) ) from TARSKI:sch 1(A3);
take X ; :: thesis: for x being set holds
( x in X iff ex M, N being strict feasible MSAlgebra of 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 ) )
thus for x being set holds
( x in X iff ex M, N being strict feasible MSAlgebra of 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 ) ) :: thesis: verum

proof

let x be set ; :: thesis: ( x in X iff ex M, N being strict feasible MSAlgebra of 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 of 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 x in X ; :: thesis: ex M, N being strict feasible MSAlgebra of 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 ex y being set st
( y in [:(Funcs ( the carrier of S,(bool A))),(Funcs ( the carrier' of S,(PFuncs ((PFuncs (NAT,A)),A)))),(Funcs ( the carrier of S,(bool A))),(Funcs ( the carrier' of S,(PFuncs ((PFuncs (NAT,A)),A)))),(Funcs ( the carrier of S,(PFuncs ((union (bool A)),(union (bool A)))))):] & S₁[y,x] ) by A4;
hence ex M, N being strict feasible MSAlgebra of 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 ) ; :: thesis: verum

end;

given M, N being strict feasible MSAlgebra of S, F being ManySortedFunction of M,N such that A5: M = i and
A6: N = j and
A7: ( F = x & the Sorts of M is_transformable_to the Sorts of N & F is_homomorphism M,N ) ; :: thesis: x in X
set y = [ the Sorts of M, the Charact of M, the Sorts of N, the Charact of N,F];
A8: ( the Sorts of N in Funcs ( the carrier of S,(bool A)) & the Charact of N in Funcs ( the carrier' of S,(PFuncs ((PFuncs (NAT,A)),A))) ) by A2, A6, Th2;
A9: dom F = the carrier of S by PARTFUN1:def 2;
rng F c= PFuncs ((union (bool A)),(union (bool A)))

proof

A10: ex M9 being strict feasible MSAlgebra of S st
( M9 = M & ( for C being Component of the Sorts of M9 holds C c= A ) ) by A1, A5, Def2;
A11: rng the Sorts of M c= bool A

proof

let x be set ; :: 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 A10;
hence x in bool A ; :: thesis: verum

end;

let w be set ; :: 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 set such that
A12: w1 in dom F and
A13: 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 A9, A12, A13, PBOOLE:def 15;
A14: dom the Sorts of M = the carrier of S by PARTFUN1:def 2;
A15: dom w9 c= union (bool A)

proof

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

end;

A17: ex N9 being strict feasible MSAlgebra of S st
( N9 = N & ( for C being Component of the Sorts of N9 holds C c= A ) ) by A2, A6, Def2;
A18: rng the Sorts of N c= bool A

proof

let x be set ; :: 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 A17;
hence x in bool A ; :: thesis: verum

end;

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

proof

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

end;

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

end;

then A21: F in Funcs ( the carrier of S,(PFuncs ((union (bool A)),(union (bool A))))) by A9, FUNCT_2:def 2;
( the Sorts of M in Funcs ( the carrier of S,(bool A)) & the Charact of M in Funcs ( the carrier' of S,(PFuncs ((PFuncs (NAT,A)),A))) ) by A1, A5, Th2;
then [ the Sorts of M, the Charact of M, the Sorts of N, the Charact of N,F] in [:(Funcs ( the carrier of S,(bool A))),(Funcs ( the carrier' of S,(PFuncs ((PFuncs (NAT,A)),A)))),(Funcs ( the carrier of S,(bool A))),(Funcs ( the carrier' of S,(PFuncs ((PFuncs (NAT,A)),A)))),(Funcs ( the carrier of S,(PFuncs ((union (bool A)),(union (bool A)))))):] by A8, A21, MCART_2:29;
hence x in X by A4, A5, A6, A7; :: thesis: verum

end;