set f = the Function of X,Y;
take p = <* the Function of X,Y*>; :: thesis: ( firstdom p = X & lastrng p c= Y )
A2: ( p ^ {} = p & {} ^ p = p ) by FINSEQ_1:34;
( dom the Function of X,Y = X & rng the Function of X,Y c= Y ) by A1, FUNCT_2:def 1;
hence ( firstdom p = X & lastrng p c= Y ) by A2, Th57; :: thesis: verum