let F1, F2 be MSFunctionSet of U1,U1; :: thesis: ( ( for h being ManySortedFunction of U1,U1 holds

( h in F1 iff h is_isomorphism U1,U1 ) ) & ( for h being ManySortedFunction of U1,U1 holds

( h in F2 iff h is_isomorphism U1,U1 ) ) implies F1 = F2 )

assume that

A3: for h being ManySortedFunction of U1,U1 holds

( h in F1 iff h is_isomorphism U1,U1 ) and

A4: for h being ManySortedFunction of U1,U1 holds

( h in F2 iff h is_isomorphism U1,U1 ) ; :: thesis: F1 = F2

thus F1 c= F2 :: according to XBOOLE_0:def 10 :: thesis: F2 c= F1

assume A6: q in F2 ; :: thesis: q in F1

then reconsider h1 = q as ManySortedFunction of U1,U1 by Th19;

h1 is_isomorphism U1,U1 by A4, A6;

hence q in F1 by A3; :: thesis: verum

( h in F1 iff h is_isomorphism U1,U1 ) ) & ( for h being ManySortedFunction of U1,U1 holds

( h in F2 iff h is_isomorphism U1,U1 ) ) implies F1 = F2 )

assume that

A3: for h being ManySortedFunction of U1,U1 holds

( h in F1 iff h is_isomorphism U1,U1 ) and

A4: for h being ManySortedFunction of U1,U1 holds

( h in F2 iff h is_isomorphism U1,U1 ) ; :: thesis: F1 = F2

thus F1 c= F2 :: according to XBOOLE_0:def 10 :: thesis: F2 c= F1

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in F2 or q in F1 )
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in F1 or q in F2 )

assume A5: q in F1 ; :: thesis: q in F2

then reconsider h1 = q as ManySortedFunction of U1,U1 by Th19;

h1 is_isomorphism U1,U1 by A3, A5;

hence q in F2 by A4; :: thesis: verum

end;assume A5: q in F1 ; :: thesis: q in F2

then reconsider h1 = q as ManySortedFunction of U1,U1 by Th19;

h1 is_isomorphism U1,U1 by A3, A5;

hence q in F2 by A4; :: thesis: verum

assume A6: q in F2 ; :: thesis: q in F1

then reconsider h1 = q as ManySortedFunction of U1,U1 by Th19;

h1 is_isomorphism U1,U1 by A4, A6;

hence q in F1 by A3; :: thesis: verum