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