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

proof

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

end;

now :: thesis: for x being object st x in dom <:f,Z,Y:> holds
<:f,Z,Y:> . x = <:f,X,Y:> . x

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

end;

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