let x be set ; :: thesis: for f, g being Function st x in dom f & g = f . x holds
( x in dom (doms f) & (doms f) . x = dom g & x in dom (rngs f) & (rngs f) . x = rng g )
let f, g be Function; :: thesis: ( x in dom f & g = f . x implies ( x in dom (doms f) & (doms f) . x = dom g & x in dom (rngs f) & (rngs f) . x = rng g ) )
assume that
A1: x in dom f and
A2: g = f . x ; :: thesis: ( x in dom (doms f) & (doms f) . x = dom g & x in dom (rngs f) & (rngs f) . x = rng g )
g in rng f by A1, A2, FUNCT_1:def 3;
then g in SubFuncs (rng f) by Def1;
then x in f " (SubFuncs (rng f)) by A1, A2, FUNCT_1:def 7;
hence ( x in dom (doms f) & (doms f) . x = dom g & x in dom (rngs f) & (rngs f) . x = rng g ) by A2, Def2, Def3; :: thesis: verum