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:> )
assume A4: x in dom <:f,X,Y:> ; :: thesis: x in dom <:g,X,Y:>
then ( x in dom f & dom f c= dom g & dom <:f,X,Y:> c= X ) by A1, A2, RELAT_1:25;
then ( x in dom g & x in X & f . x in Y & f . x = g . x ) by A1, A4, Th78, GRFUNC_1:8;
hence x in dom <:g,X,Y:> by 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 x in dom <:f,X,Y:> ; :: thesis: <:f,X,Y:> . x = <:g,X,Y:> . x
then ( <:f,X,Y:> . x = f . x & <:g,X,Y:> . x = g . x & f . x = g . x ) by A1, A2, A3, Th80, GRFUNC_1:8;
hence <:f,X,Y:> . x = <:g,X,Y:> . x ; :: thesis: verum

end;

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