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 f & f1 = f \/ g holds

f1 /. c = f /. c

let c be Element of C; :: thesis: for f, f1, g being PartFunc of C,D st c in dom f & f1 = f \/ g holds

f1 /. c = f /. c

let f, f1, g be PartFunc of C,D; :: thesis: ( c in dom f & f1 = f \/ g implies f1 /. c = f /. c )

assume that

A1: c in dom f and

A2: f1 = f \/ g ; :: thesis: f1 /. c = f /. c

[c,(f . c)] in f by A1, FUNCT_1:1;

then [c,(f . c)] in f1 by A2, XBOOLE_0:def 3;

then A3: c in dom f1 by FUNCT_1:1;

f1 . c = f . c by A1, A2, GRFUNC_1:15;

then f1 /. c = f . c by A3, PARTFUN1:def 6;

hence f1 /. c = f /. c by A1, PARTFUN1:def 6; :: thesis: verum

for f, f1, g being PartFunc of C,D st c in dom f & f1 = f \/ g holds

f1 /. c = f /. c

let c be Element of C; :: thesis: for f, f1, g being PartFunc of C,D st c in dom f & f1 = f \/ g holds

f1 /. c = f /. c

let f, f1, g be PartFunc of C,D; :: thesis: ( c in dom f & f1 = f \/ g implies f1 /. c = f /. c )

assume that

A1: c in dom f and

A2: f1 = f \/ g ; :: thesis: f1 /. c = f /. c

[c,(f . c)] in f by A1, FUNCT_1:1;

then [c,(f . c)] in f1 by A2, XBOOLE_0:def 3;

then A3: c in dom f1 by FUNCT_1:1;

f1 . c = f . c by A1, A2, GRFUNC_1:15;

then f1 /. c = f . c by A3, PARTFUN1:def 6;

hence f1 /. c = f /. c by A1, PARTFUN1:def 6; :: thesis: verum