let it1, it2 be set ; :: thesis: ( ( ( for i being set st i in I & B . i = {} holds

A . i = {} ) & ( for x being set holds

( x in it1 iff x is ManySortedFunction of A,B ) ) & ( for x being set holds

( x in it2 iff x is ManySortedFunction of A,B ) ) implies it1 = it2 ) & ( ex i being set st

( i in I & B . i = {} & not A . i = {} ) & it1 = {} & it2 = {} implies it1 = it2 ) )

( i in I & B . i = {} & not A . i = {} ) & it1 = {} & it2 = {} implies it1 = it2 ) ; :: thesis: verum

A . i = {} ) & ( for x being set holds

( x in it1 iff x is ManySortedFunction of A,B ) ) & ( for x being set holds

( x in it2 iff x is ManySortedFunction of A,B ) ) implies it1 = it2 ) & ( ex i being set st

( i in I & B . i = {} & not A . i = {} ) & it1 = {} & it2 = {} implies it1 = it2 ) )

hereby :: thesis: ( ex i being set st

( i in I & B . i = {} & not A . i = {} ) & it1 = {} & it2 = {} implies it1 = it2 )

thus
( ex i being set st ( i in I & B . i = {} & not A . i = {} ) & it1 = {} & it2 = {} implies it1 = it2 )

assume
for i being set st i in I & B . i = {} holds

A . i = {} ; :: thesis: ( ( for x being set holds

( x in it1 iff x is ManySortedFunction of A,B ) ) & ( for x being set holds

( x in it2 iff x is ManySortedFunction of A,B ) ) implies it1 = it2 )

assume that

A16: for x being set holds

( x in it1 iff x is ManySortedFunction of A,B ) and

A17: for x being set holds

( x in it2 iff x is ManySortedFunction of A,B ) ; :: thesis: it1 = it2

end;A . i = {} ; :: thesis: ( ( for x being set holds

( x in it1 iff x is ManySortedFunction of A,B ) ) & ( for x being set holds

( x in it2 iff x is ManySortedFunction of A,B ) ) implies it1 = it2 )

assume that

A16: for x being set holds

( x in it1 iff x is ManySortedFunction of A,B ) and

A17: for x being set holds

( x in it2 iff x is ManySortedFunction of A,B ) ; :: thesis: it1 = it2

now :: thesis: for x being object holds

( x in it1 iff x in it2 )

hence
it1 = it2
by TARSKI:2; :: thesis: verum( x in it1 iff x in it2 )

let x be object ; :: thesis: ( x in it1 iff x in it2 )

( x in it1 iff x is ManySortedFunction of A,B ) by A16;

hence ( x in it1 iff x in it2 ) by A17; :: thesis: verum

end;( x in it1 iff x is ManySortedFunction of A,B ) by A16;

hence ( x in it1 iff x in it2 ) by A17; :: thesis: verum

( i in I & B . i = {} & not A . i = {} ) & it1 = {} & it2 = {} implies it1 = it2 ) ; :: thesis: verum