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 ) )

hereby :: thesis: ( 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

now :: thesis: for x being object holds
( 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;

hence it1 = it2 by TARSKI:2; :: thesis: verum

end;

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