let X, Y be set ; :: thesis: for f, g being Function st f c= g holds
<:f,X,Y:> c= <:g,X,Y:>
let f, g be Function; :: thesis: ( f c= g implies <:f,X,Y:> c= <:g,X,Y:> )
assume A1: f c= g ; :: thesis: <:f,X,Y:> c= <:g,X,Y:>
A2: dom <:f,X,Y:> c= dom f by Th77;

now

thus A3: dom <:f,X,Y:> c= dom <:g,X,Y:> :: thesis: for x being set st x in dom <:f,X,Y:> holds
<:f,X,Y:> . x = <:g,X,Y:> . x

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom <:f,X,Y:> or x in dom <:g,X,Y:> )
A4: dom f c= dom g by A1, RELAT_1:25;
assume A5: x in dom <:f,X,Y:> ; :: thesis: x in dom <:g,X,Y:>
then A6: f . x = g . x by A1, A2, GRFUNC_1:8;
( x in dom f & f . x in Y ) by A5, Th78;
hence x in dom <:g,X,Y:> by A5, A4, A6, Th78; :: thesis: verum

end;

let x be set ; :: thesis: ( x in dom <:f,X,Y:> implies <:f,X,Y:> . x = <:g,X,Y:> . x )
assume A7: x in dom <:f,X,Y:> ; :: thesis: <:f,X,Y:> . x = <:g,X,Y:> . x
then A8: <:f,X,Y:> . x = f . x by Th80;
<:g,X,Y:> . x = g . x by A3, A7, Th80;
hence <:f,X,Y:> . x = <:g,X,Y:> . x by A1, A2, A7, A8, GRFUNC_1:8; :: thesis: verum

end;

hence <:f,X,Y:> c= <:g,X,Y:> by GRFUNC_1:8; :: thesis: verum