let g be Function-yielding Function; for X being Function
for d being object holds dom (NDentry (g,X,d)) = rng X
let X be Function; for d being object holds dom (NDentry (g,X,d)) = rng X
let d be object ; 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
XBOOLE_0:def 10 rng X c= dom (NDentry (g,X,d))proof
let x be
object ;
TARSKI:def 3 ( not x in dom (NDentry (g,X,d)) or x in rng X )
assume
x in dom (NDentry (g,X,d))
;
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;
verum
end;
let x be object ; TARSKI:def 3 ( not x in rng X or x in dom (NDentry (g,X,d)) )
assume
x in rng X
; 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; verum