let Y be set ; :: thesis: for f, g being Y -valued Function st f c= g holds

for x being set st x in dom f holds

f /. x = g /. x

let f, g be Y -valued Function; :: thesis: ( f c= g implies for x being set st x in dom f holds

f /. x = g /. x )

assume A1: f c= g ; :: thesis: for x being set st x in dom f holds

f /. x = g /. x

then A2: dom f c= dom g by GRFUNC_1:2;

let x be set ; :: thesis: ( x in dom f implies f /. x = g /. x )

assume A3: x in dom f ; :: thesis: f /. x = g /. x

then f . x = g . x by A1, GRFUNC_1:2;

then f /. x = g . x by A3, PARTFUN1:def 6;

hence f /. x = g /. x by A2, A3, PARTFUN1:def 6; :: thesis: verum

for x being set st x in dom f holds

f /. x = g /. x

let f, g be Y -valued Function; :: thesis: ( f c= g implies for x being set st x in dom f holds

f /. x = g /. x )

assume A1: f c= g ; :: thesis: for x being set st x in dom f holds

f /. x = g /. x

then A2: dom f c= dom g by GRFUNC_1:2;

let x be set ; :: thesis: ( x in dom f implies f /. x = g /. x )

assume A3: x in dom f ; :: thesis: f /. x = g /. x

then f . x = g . x by A1, GRFUNC_1:2;

then f /. x = g . x by A3, PARTFUN1:def 6;

hence f /. x = g /. x by A2, A3, PARTFUN1:def 6; :: thesis: verum