let X, Y be set ; for f, g being Function st f c= g holds
<:f,X,Y:> c= <:g,X,Y:>
let f, g be Function; ( f c= g implies <:f,X,Y:> c= <:g,X,Y:> )
assume A1:
f c= g
; <:f,X,Y:> c= <:g,X,Y:>
A2:
dom <:f,X,Y:> c= dom f
by Th23;
now ( dom <:f,X,Y:> c= dom <:g,X,Y:> & ( for x being object st x in dom <:f,X,Y:> holds
<:f,X,Y:> . x = <:g,X,Y:> . x ) )thus A3:
dom <:f,X,Y:> c= dom <:g,X,Y:>
for x being object st x in dom <:f,X,Y:> holds
<:f,X,Y:> . x = <:g,X,Y:> . xproof
let x be
object ;
TARSKI:def 3 ( not x in dom <:f,X,Y:> or x in dom <:g,X,Y:> )
A4:
dom f c= dom g
by A1, RELAT_1:11;
assume A5:
x in dom <:f,X,Y:>
;
x in dom <:g,X,Y:>
then A6:
f . x = g . x
by A1, A2, GRFUNC_1:2;
(
x in dom f &
f . x in Y )
by A5, Th24;
hence
x in dom <:g,X,Y:>
by A5, A4, A6, Th24;
verum
end; let x be
object ;
( x in dom <:f,X,Y:> implies <:f,X,Y:> . x = <:g,X,Y:> . x )assume A7:
x in dom <:f,X,Y:>
;
<:f,X,Y:> . x = <:g,X,Y:> . xthen A8:
<:f,X,Y:> . x = f . x
by Th26;
<:g,X,Y:> . x = g . x
by A3, A7, Th26;
hence
<:f,X,Y:> . x = <:g,X,Y:> . x
by A1, A2, A7, A8, GRFUNC_1:2;
verum end;
hence
<:f,X,Y:> c= <:g,X,Y:>
by GRFUNC_1:2; verum