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 f1 & f1 = f \/ g & not f1 /. c = f /. c 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 f1 & f1 = f \/ g & not f1 /. c = f /. c holds
f1 /. c = g /. c
let f, f1, g be PartFunc of C,D; :: thesis: ( c in dom f1 & f1 = f \/ g & not f1 /. c = f /. c implies f1 /. c = g /. c )
assume that
A1: c in dom f1 and
A2: f1 = f \/ g ; :: thesis: ( f1 /. c = f /. c or f1 /. c = g /. c )
[c,(f1 /. c)] in f1 by A1, Th46;
then A3: ( [c,(f1 /. c)] in f or [c,(f1 /. c)] in g ) by A2, XBOOLE_0:def 3;

now :: thesis: ( f1 /. c = f /. c or f1 /. c = g /. c )

per cases ( c in dom f or c in dom g ) by A3, FUNCT_1:1;

suppose c in dom f ; :: thesis: ( f1 /. c = f /. c or f1 /. c = g /. c )

then [c,(f /. c)] in f by Th46;
then [c,(f /. c)] in f1 by A2, XBOOLE_0:def 3;
hence ( f1 /. c = f /. c or f1 /. c = g /. c ) by Th46; :: thesis: verum

end;

suppose c in dom g ; :: thesis: ( f1 /. c = f /. c or f1 /. c = g /. c )

then [c,(g /. c)] in g by Th46;
then [c,(g /. c)] in f1 by A2, XBOOLE_0:def 3;
hence ( f1 /. c = f /. c or f1 /. c = g /. c ) by Th46; :: thesis: verum

end;

end;

end;

hence ( f1 /. c = f /. c or f1 /. c = g /. c ) ; :: thesis: verum