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;

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 )

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