let f, g be Function; :: thesis: ( f c= g iff ( dom f c= dom g & ( for x being set st x in dom f holds
f . x = g . x ) ) )
thus ( f c= g implies ( dom f c= dom g & ( for x being set st x in dom f holds
f . x = g . x ) ) ) :: thesis: ( dom f c= dom g & ( for x being set st x in dom f holds
f . x = g . x ) implies f c= g )

proof

assume A1: f c= g ; :: thesis: ( dom f c= dom g & ( for x being set st x in dom f holds
f . x = g . x ) )
hence dom f c= dom g by RELAT_1:25; :: thesis: for x being set st x in dom f holds
f . x = g . x
let x be set ; :: thesis: ( x in dom f implies f . x = g . x )
assume x in dom f ; :: thesis: f . x = g . x
then [x,(f . x)] in f by FUNCT_1:def 4;
hence f . x = g . x by A1, FUNCT_1:8; :: thesis: verum

end;

assume that
A2: dom f c= dom g and
A3: for x being set st x in dom f holds
f . x = g . x ; :: thesis: f c= g
let x be set ; :: according to RELAT_1:def 3 :: thesis: for b₁ being set holds
( not [x,b₁] in f or [x,b₁] in g )
let y be set ; :: thesis: ( not [x,y] in f or [x,y] in g )
assume [x,y] in f ; :: thesis: [x,y] in g
then ( y = f . x & x in dom f ) by FUNCT_1:8;
then ( y = g . x & x in dom g ) by A2, A3;
hence [x,y] in g by FUNCT_1:def 4; :: thesis: verum