let C, D be non empty set ; :: thesis: for c being Element of C
for f1, f, 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 f1, f, 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 f1, f, 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 A1: ( c in dom f1 & f1 = f \/ g ) ; :: thesis: ( f1 /. c = f /. c or f1 /. c = g /. c )
then [c,(f1 /. c)] in f1 by Th65;
then A2: ( [c,(f1 /. c)] in f or [c,(f1 /. c)] in g ) by A1, XBOOLE_0:def 3;

now

per cases ( c in dom f or c in dom g ) by A2, FUNCT_1:8;

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

then [c,(f /. c)] in f by Th65;
then [c,(f /. c)] in f1 by A1, XBOOLE_0:def 3;
hence ( f1 /. c = f /. c or f1 /. c = g /. c ) by Th65; :: 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 Th65;
then [c,(g /. c)] in f1 by A1, XBOOLE_0:def 3;
hence ( f1 /. c = f /. c or f1 /. c = g /. c ) by Th65; :: thesis: verum

end;

end;

end;

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