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 S1[ 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))))) & S1[x] ) )
from XBOOLE_0:sch 1();
take
X
; 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 ; ( 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 ( 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
;
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;
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;
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;
( 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;
( 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;
f is_homomorphism M,Nthus
f is_homomorphism M,
N
by A10;
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 )
; 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)))
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; verum