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