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

deffunc H₁( object ) -> set = Funcs ((A . $1),(B . $1));
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 )
consider F being ManySortedSet of I such that
A2: for i being object 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 object st i in dom F holds
g . i in F . i by CARD_3:def 5;
A6: for i being object st i in I holds
g . i is Function of (A . i),(B . i)

proof

let i be object ; :: 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)
( dom F = I & F . i = Funcs ((A . i),(B . i)) ) by A2, A7, PARTFUN1:def 2;
hence g . i is Function of (A . i),(B . i) by A5, A7, FUNCT_2:66; :: thesis: verum

end;

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

end;

assume A8: x is ManySortedFunction of A,B ; :: thesis: x in product F
then reconsider g = x as ManySortedSet of I ;
A9: 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 A10: i in I ; :: thesis: g . i in Funcs ((A . i),(B . i))
then A11: ( B . i = {} implies A . i = {} ) by A1;
g . i is Function of (A . i),(B . i) by A8, A10, PBOOLE:def 15;
hence g . i in Funcs ((A . i),(B . i)) by A11, FUNCT_2:8; :: thesis: verum

end;

A12: 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 A13: 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 A9, A13; :: thesis: verum

end;

A14: for i being object st i in dom F holds
g . i in F . i

proof

A15: dom F = I by PARTFUN1:def 2;
let i be object ; :: thesis: ( i in dom F implies g . i in F . i )
assume i in dom F ; :: thesis: g . i in F . i
hence g . i in F . i by A12, A15; :: thesis: verum

end;

dom g = I by PARTFUN1:def 2;
then dom g = dom F by PARTFUN1:def 2;
hence x in product F by A14, 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