set T = the Sorts of U1;
let F1, F2 be MSFunctionSet of the Sorts of U1, the Sorts of U1; :: thesis: ( ( for f being Element of F1 holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds
( h in F1 iff h is_homomorphism U1,U1 ) ) & ( for f being Element of F2 holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds
( h in F2 iff h is_homomorphism U1,U1 ) ) implies F1 = F2 )
assume that
A3: for f being Element of F1 holds f is ManySortedFunction of U1,U1 and
A4: for h being ManySortedFunction of U1,U1 holds
( h in F1 iff h is_homomorphism U1,U1 ) and
A5: for f being Element of F2 holds f is ManySortedFunction of U1,U1 and
A6: for h being ManySortedFunction of U1,U1 holds
( h in F2 iff h is_homomorphism U1,U1 ) ; :: thesis: F1 = F2
A7: F2 c= F1

proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in F2 or q in F1 )
assume A8: q in F2 ; :: thesis: q in F1
then reconsider h1 = q as ManySortedFunction of U1,U1 by A5;
h1 is_homomorphism U1,U1 by A6, A8;
hence q in F1 by A4; :: thesis: verum

end;

F1 c= F2

proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in F1 or q in F2 )
assume A9: q in F1 ; :: thesis: q in F2
then reconsider h1 = q as ManySortedFunction of U1,U1 by A3;
h1 is_homomorphism U1,U1 by A4, A9;
hence q in F2 by A6; :: thesis: verum

end;

hence F1 = F2 by A7, XBOOLE_0:def 10; :: thesis: verum