let x be set ; :: thesis: for g, f being Function st g in rng f & ( for g being Function st g in rng f holds
x in dom g ) holds
x in dom <:f:>
let g, f be Function; :: thesis: ( g in rng f & ( for g being Function st g in rng f holds
x in dom g ) implies x in dom <:f:> )
assume that
A1: g in rng f and
A2: for g being Function st g in rng f holds
x in dom g ; :: thesis: x in dom <:f:>
ex y being set st
( y in dom f & g = f . y ) by A1, FUNCT_1:def 5;
then A3: doms f <> {} by Th31, RELAT_1:60;

A4: now

let y be set ; :: thesis: ( y in dom (doms f) implies x in (doms f) . y )
assume y in dom (doms f) ; :: thesis: x in (doms f) . y
then A5: y in f " (SubFuncs (rng f)) by Def2;
then f . y in SubFuncs (rng f) by FUNCT_1:def 13;
then reconsider g = f . y as Function by Def1;
A6: y in dom f by A5, FUNCT_1:def 13;
then g in rng f by FUNCT_1:def 5;
then x in dom g by A2;
hence x in (doms f) . y by A6, Th31; :: thesis: verum

end;

dom <:f:> = meet (doms f) by Th49;
hence x in dom <:f:> by A3, A4, Th37; :: thesis: verum