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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom <:f,X,Z:> or x in dom <:f,X,Y:> )
assume A3: x in dom <:f,X,Z:> ; :: thesis: x in dom <:f,X,Y:>
then f . x in Z by Th78;
then ( x in dom f & x in X & f . x in Y ) by A1, A3, Th78;
hence x in dom <:f,X,Y:> by Th78; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in dom <:f,X,Z:> implies <:f,X,Z:> . x = <:f,X,Y:> . x )
assume x in dom <:f,X,Z:> ; :: thesis: <:f,X,Z:> . x = <:f,X,Y:> . x
then ( <:f,X,Z:> . x = f . x & x in dom <:f,X,Y:> ) by A2, Th80;
hence <:f,X,Z:> . x = <:f,X,Y:> . x by Th80; :: thesis: verum

end;

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