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

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

( dom (pr1 X,Y) = [:X,Y:] & rng (pr1 X,Y) c= X ) by Def5, Th59;
hence pr1 X,Y is Function of [:X,Y:],X by A1, FUNCT_2:def 1, RELSET_1:11; :: thesis: verum

end;

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

hence pr1 X,Y is Function of [:X,Y:],X by ZFMISC_1:113; :: thesis: verum

end;

end;