let C, D be non empty set ; for c being Element of C
for f, f1, g being PartFunc of C,D st c in dom g & f1 = f \/ g holds
f1 /. c = g /. c
let c be Element of C; for f, f1, g being PartFunc of C,D st c in dom g & f1 = f \/ g holds
f1 /. c = g /. c
let f, f1, g be PartFunc of C,D; ( c in dom g & f1 = f \/ g implies f1 /. c = g /. c )
assume that
A1:
c in dom g
and
A2:
f1 = f \/ g
; f1 /. c = g /. c
[c,(g . c)] in g
by A1, FUNCT_1:1;
then
[c,(g . c)] in f1
by A2, XBOOLE_0:def 3;
then A3:
c in dom f1
by FUNCT_1:1;
f1 . c = g . c
by A1, A2, GRFUNC_1:15;
then
f1 /. c = g . c
by A3, PARTFUN1:def 6;
hence
f1 /. c = g /. c
by A1, PARTFUN1:def 6; verum