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 A18: ( ( 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 ) ) ) ; :: thesis: it1 = it2

now

let x be set ; :: thesis: ( x in it1 iff x in it2 )
( ( x in it1 implies x is ManySortedFunction of A,B ) & ( x is ManySortedFunction of A,B implies x in it1 ) & ( x in it2 implies x is ManySortedFunction of A,B ) & ( x is ManySortedFunction of A,B implies x in it2 ) ) by A18;
hence ( x in it1 iff x in it2 ) ; :: 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