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:7;
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 4;
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 5;
reconsider w9 = w as Function of (the Sorts of M . w1),(the Sorts of N . w1) by A9, A12, A13, PBOOLE:def 18;
A14: dom the Sorts of M = the carrier of S by PARTFUN1:def 4;
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 5;
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 4;
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 5;
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 5; :: 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:31;
hence x in X by A4, A5, A6, A7; :: thesis: verum

end;