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

suppose ( 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 Def4, Th43;
hence pr1 (X,Y) is Function of [:X,Y:],X by FUNCT_2:2; :: 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:90; :: thesis: verum

end;

end;