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 M' being strict feasible MSAlgebra of S st
( M' = M & ( for C being Component of the Sorts of M' 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 x' = x as Component of the Sorts of M ;
x' 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 w' = 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 w' c= union (bool A)

proof

let s be set ; :: according to TARSKI:def 3 :: thesis: ( not s in dom w' or s in union (bool A) )
assume A16: s in dom w' ; :: 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 N' being strict feasible MSAlgebra of S st
( N' = N & ( for C being Component of the Sorts of N' 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 x' = x as Component of the Sorts of N ;
x' 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 w' c= union (bool A)

proof

let r be set ; :: according to TARSKI:def 3 :: thesis: ( not r in rng w' or r in union (bool A) )
assume A20: r in rng w' ; :: 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;