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