thus ( ( for i being set st i in I & B . i = {} holds
A . i = {} ) implies ex IT being set st
for x being set holds
( x in IT iff x is ManySortedFunction of A,B ) ) :: thesis: ( ex i being set st
( i in I & B . i = {} & not A . i = {} ) implies ex b₁ being set st b₁ = {} )

proof

assume A1: for i being set st i in I & B . i = {} holds
A . i = {} ; :: thesis: ex IT being set st
for x being set holds
( x in IT iff x is ManySortedFunction of A,B )
deffunc H₁( set ) -> set = Funcs (A . $1),(B . $1);
consider F being ManySortedSet of such that
A2: for i being set st i in I holds
F . i = H₁(i) from PBOOLE:sch 4();
take product F ; :: thesis: for x being set holds
( x in product F iff x is ManySortedFunction of A,B )
let x be set ; :: thesis: ( x in product F iff x is ManySortedFunction of A,B )
thus ( x in product F implies x is ManySortedFunction of A,B ) :: thesis: ( x is ManySortedFunction of A,B implies x in product F )

proof

assume x in product F ; :: thesis: x is ManySortedFunction of A,B
then consider g being Function such that
A3: x = g and
A4: dom g = dom F and
A5: for i being set st i in dom F holds
g . i in F . i by CARD_3:def 5;
A6: for i being set st i in I holds
g . i is Function of (A . i),(B . i)

proof

let i be set ; :: thesis: ( i in I implies g . i is Function of (A . i),(B . i) )
assume A7: i in I ; :: thesis: g . i is Function of (A . i),(B . i)
A8: dom F = I by PARTFUN1:def 4;
F . i = Funcs (A . i),(B . i) by A2, A7;
hence g . i is Function of (A . i),(B . i) by A5, A7, A8, FUNCT_2:121; :: thesis: verum

end;

dom F = I by PARTFUN1:def 4;
then reconsider g = g as ManySortedSet of by A4, PARTFUN1:def 4, RELAT_1:def 18;
g is ManySortedFunction of A,B by A6, PBOOLE:def 18;
hence x is ManySortedFunction of A,B by A3; :: thesis: verum

end;

assume A9: x is ManySortedFunction of A,B ; :: thesis: x in product F
then reconsider g = x as ManySortedSet of ;
A10: dom g = I by PARTFUN1:def 4;
A11: for i being set st i in I holds
g . i in Funcs (A . i),(B . i)

proof

let i be set ; :: thesis: ( i in I implies g . i in Funcs (A . i),(B . i) )
assume A12: i in I ; :: thesis: g . i in Funcs (A . i),(B . i)
then A13: g . i is Function of (A . i),(B . i) by A9, PBOOLE:def 18;
( B . i = {} implies A . i = {} ) by A1, A12;
hence g . i in Funcs (A . i),(B . i) by A13, FUNCT_2:11; :: thesis: verum

end;

A14: for i being set st i in I holds
g . i in F . i

proof

let i be set ; :: thesis: ( i in I implies g . i in F . i )
assume A15: i in I ; :: thesis: g . i in F . i
then F . i = Funcs (A . i),(B . i) by A2;
hence g . i in F . i by A11, A15; :: thesis: verum

end;

A16: for i being set st i in dom F holds
g . i in F . i

proof

let i be set ; :: thesis: ( i in dom F implies g . i in F . i )
assume A17: i in dom F ; :: thesis: g . i in F . i
dom F = I by PARTFUN1:def 4;
hence g . i in F . i by A14, A17; :: thesis: verum

end;

dom g = dom F by A10, PARTFUN1:def 4;
hence x in product F by A16, CARD_3:def 5; :: thesis: verum

end;

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