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