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