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

f /. c = g /. c ) holds

f c= g

let f, g be PartFunc of C,D; :: 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 )

assume that

A1: dom f c= dom g and

A2: for c being Element of C st c in dom f holds

f /. c = g /. c ; :: thesis: f c= g

f /. c = g /. c ) holds

f c= g

let f, g be PartFunc of C,D; :: 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 )

assume that

A1: dom f c= dom g and

A2: for c being Element of C st c in dom f holds

f /. c = g /. c ; :: thesis: f c= g

now :: thesis: for x being object st x in dom f holds

f . x = g . x

hence
f c= g
by A1, GRFUNC_1:2; :: thesis: verumf . x = g . x

let x be object ; :: thesis: ( x in dom f implies f . x = g . x )

assume A3: x in dom f ; :: thesis: f . x = g . x

then reconsider x1 = x as Element of C ;

f /. x1 = g /. x1 by A2, A3;

then f . x = g /. x1 by A3, PARTFUN1:def 6;

hence f . x = g . x by A1, A3, PARTFUN1:def 6; :: thesis: verum

end;assume A3: x in dom f ; :: thesis: f . x = g . x

then reconsider x1 = x as Element of C ;

f /. x1 = g /. x1 by A2, A3;

then f . x = g /. x1 by A3, PARTFUN1:def 6;

hence f . x = g . x by A1, A3, PARTFUN1:def 6; :: thesis: verum