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 g & f1 = f \/ g holds
f1 /. c = g /. c
let c be Element of C; :: thesis: 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; :: thesis: ( c in dom g & f1 = f \/ g implies f1 /. c = g /. c )
assume that
A1: c in dom g and
A2: f1 = f \/ g ; :: thesis: 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; :: thesis: verum