let g be Function-yielding Function; :: thesis: for X being Function
for d being object holds dom (NDentry (g,X,d)) = rng X
let X be Function; :: thesis: for d being object holds dom (NDentry (g,X,d)) = rng X
let d be object ; :: thesis: dom (NDentry (g,X,d)) = rng X
set f = NDentry (g,X,d);
set h = NDdataSeq (g,X,d);
A1: dom (NDdataSeq (g,X,d)) = dom X by Def4;
thus dom (NDentry (g,X,d)) c= rng X :: according to XBOOLE_0:def 10 :: thesis: rng X c= dom (NDentry (g,X,d))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (NDentry (g,X,d)) or x in rng X )
assume x in dom (NDentry (g,X,d)) ; :: thesis: x in rng X
then consider v being object such that
A2: [x,v] in NDentry (g,X,d) by XTUPLE_0:def 12;
consider z being object such that
A3: z in dom (NDdataSeq (g,X,d)) and
A4: (NDdataSeq (g,X,d)) . z = [x,v] by A2, FUNCT_1:def 3;
(NDdataSeq (g,X,d)) . z = [(X . z),((g . z) . d)] by A1, A3, Def4;
then X . z = x by A4, XTUPLE_0:1;
hence x in rng X by A1, A3, FUNCT_1:def 3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng X or x in dom (NDentry (g,X,d)) )
assume x in rng X ; :: thesis: x in dom (NDentry (g,X,d))
then consider z being object such that
A5: z in dom X and
A6: X . z = x by FUNCT_1:def 3;
(NDdataSeq (g,X,d)) . z = [(X . z),((g . z) . d)] by A5, Def4;
then [(X . z),((g . z) . d)] in rng (NDdataSeq (g,X,d)) by A1, A5, FUNCT_1:3;
hence x in dom (NDentry (g,X,d)) by A6, XTUPLE_0:def 12; :: thesis: verum