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 g = Y1 by FUNCT_2:def 1;
assume A2: f c= g ; :: thesis: f * c= g *
A3: dom f = X1 by FUNCT_2:def 1;
then A4: X1 * c= Y1 * by A1, A2, FINSEQ_1:62, RELAT_1:11;

A5: now :: thesis: for x being object st x in X1 * holds
(f *) . x = (g *) . x

let x be object ; :: 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 * ;
A6: (f *) . p = f * p by LANG1:def 13;
(rng p) /\ Y1 c= X1 ;
then A7: f * p = g * p by A3, A1, A2, Th2;
p in X1 * ;
hence (f *) . x = (g *) . x by A4, A6, A7, LANG1:def 13; :: thesis: verum

end;

A8: dom (g *) = Y1 * by FUNCT_2:def 1;
dom (f *) = X1 * by FUNCT_2:def 1;
hence f * c= g * by A8, A4, A5, GRFUNC_1:2; :: thesis: verum