let X1, Y1, X2, Y2 be non empty set ; :: thesis: for f being Function of X1,X2
for g being Function of Y1,Y2 st f c= g holds
f * c= g *
let f be Function of X1,X2; :: thesis: for g being Function of Y1,Y2 st f c= g holds
f * c= g *
let g be Function of Y1,Y2; :: thesis: ( f c= g implies f * c= g * )
A1: ( dom f = X1 & dom g = Y1 & dom (f * ) = X1 * & dom (g * ) = Y1 * ) by FUNCT_2:def 1;
assume A2: f c= g ; :: thesis: f * c= g *
then A3: X1 * c= Y1 * by A1, FINSEQ_1:83, RELAT_1:25;

now

let x be set ; :: thesis: ( x in X1 * implies (f * ) . x = (g * ) . x )
assume x in X1 * ; :: thesis: (f * ) . x = (g * ) . x
then reconsider p = x as Element of X1 * ;
( (rng p) /\ Y1 c= X1 & p in X1 * ) ;
then ( (f * ) . p = f * p & p in Y1 * & f * p = g * p ) by A1, A2, A3, Th2, LANG1:def 14;
hence (f * ) . x = (g * ) . x by LANG1:def 14; :: thesis: verum

end;

hence f * c= g * by A1, A3, GRFUNC_1:8; :: thesis: verum