let D, C be non empty set ; :: thesis: for f, g being PartFunc of C,D holds
( f c= g iff ( dom f c= dom g & ( for c being Element of C st c in dom f holds
f /. c = g /. c ) ) )
let f, g be PartFunc of C,D; :: thesis: ( f c= g iff ( dom f c= dom g & ( for c being Element of C st c in dom f holds
f /. c = g /. c ) ) )
thus ( f c= g implies ( dom f c= dom g & ( for c being Element of C st c in dom f holds
f /. c = g /. c ) ) ) :: thesis: ( dom f c= dom g & ( for c being Element of C st c in dom f holds
f /. c = g /. c ) implies f c= g )

proof

assume A1: f c= g ; :: thesis: ( dom f c= dom g & ( for c being Element of C st c in dom f holds
f /. c = g /. c ) )
then A2: ( dom f c= dom g & ( for x being set st x in dom f holds
f . x = g . x ) ) by GRFUNC_1:8;
thus dom f c= dom g by A1, GRFUNC_1:8; :: thesis: for c being Element of C st c in dom f holds
f /. c = g /. c
let c be Element of C; :: thesis: ( c in dom f implies f /. c = g /. c )
assume A3: c in dom f ; :: thesis: f /. c = g /. c
then f . c = g . c by A1, GRFUNC_1:8;
then f /. c = g . c by A3, PARTFUN1:def 8;
hence f /. c = g /. c by A2, A3, PARTFUN1:def 8; :: thesis: verum

end;

assume A4: ( dom f c= dom g & ( for c being Element of C st c in dom f holds
f /. c = g /. c ) ) ; :: thesis: f c= g

now

let x be set ; :: thesis: ( x in dom f implies f . x = g . x )
assume A5: x in dom f ; :: thesis: f . x = g . x
then reconsider x1 = x as Element of C ;
f /. x1 = g /. x1 by A4, A5;
then f . x = g /. x1 by A5, PARTFUN1:def 8;
hence f . x = g . x by A4, A5, PARTFUN1:def 8; :: thesis: verum

end;

hence f c= g by A4, GRFUNC_1:8; :: thesis: verum