per cases not ( Y = {} & not [:X,Y:] = {} & not ( Y = {} & [:X,Y:] <> {} ) ) ;

suppose A2: ( Y = {} implies [:X,Y:] = {} ) ; :: thesis: pr2 (X,Y) is Function of [:X,Y:],Y

( dom (pr2 (X,Y)) = [:X,Y:] & rng (pr2 (X,Y)) c= Y ) by Def6, Th61;
hence pr2 (X,Y) is Function of [:X,Y:],Y by A2, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum

end;

suppose ( Y = {} & [:X,Y:] <> {} ) ; :: thesis: pr2 (X,Y) is Function of [:X,Y:],Y

hence pr2 (X,Y) is Function of [:X,Y:],Y by ZFMISC_1:90; :: thesis: verum

end;

end;