let x be object ; :: thesis: for f being Function-yielding Function st x in dom <:f:> holds
for g being Function st g in rng f holds
x in dom g
let f be Function-yielding Function; :: thesis: ( x in dom <:f:> implies for g being Function st g in rng f holds
x in dom g )
assume A1: x in dom <:f:> ; :: thesis: for g being Function st g in rng f holds
x in dom g
let g be Function; :: thesis: ( g in rng f implies x in dom g )
assume g in rng f ; :: thesis: x in dom g
then consider y being object such that
A2: ( y in dom f & g = f . y ) by FUNCT_1:def 3;
( y in dom (doms f) & (doms f) . y = dom g ) by A2, Th18;
then dom g in rng (doms f) by FUNCT_1:def 3;
then A3: meet (rng (doms f)) c= dom g by SETFAM_1:3;
meet (doms f) = dom <:f:> by Th25;
hence x in dom g by A1, A3; :: thesis: verum