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:11; :: 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:113; :: thesis: verum

end;

end;