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

suppose ( 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 Def5, Th45;
hence pr2 (X,Y) is Function of [:X,Y:],Y by FUNCT_2:2; :: 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;