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