let g be Function; :: thesis: for x being object
for f being Function-yielding 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 x be object ; :: thesis: for f being Function-yielding 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 f be Function-yielding 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 object st
( y in dom f & g = f . y ) by A1, FUNCT_1:def 3;
then A3: doms f <> {} by Th18;

A4: now :: thesis: for y being object st y in dom (doms f) holds
x in (doms f) . y

let y be object ; :: 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 dom f by Def1;
reconsider g = f . y as Function ;
A6: y in dom f by A5;
then g in rng f by FUNCT_1:def 3;
then x in dom g by A2;
hence x in (doms f) . y by A6, Th18; :: thesis: verum

end;

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