let V, A be set ; :: thesis: for d being TypeSCNominativeData of V,A
for g being V,A -FPrg-yielding FinSequence
for X being one-to-one FinSequence st dom g = dom X & d in_doms g holds
rng (NDentry (g,X,d)) c= ND (V,A)
let d be TypeSCNominativeData of V,A; :: thesis: for g being V,A -FPrg-yielding FinSequence
for X being one-to-one FinSequence st dom g = dom X & d in_doms g holds
rng (NDentry (g,X,d)) c= ND (V,A)
let g be V,A -FPrg-yielding FinSequence; :: thesis: for X being one-to-one FinSequence st dom g = dom X & d in_doms g holds
rng (NDentry (g,X,d)) c= ND (V,A)
let X be one-to-one FinSequence; :: thesis: ( dom g = dom X & d in_doms g implies rng (NDentry (g,X,d)) c= ND (V,A) )
assume that
A1: dom g = dom X and
A2: d in_doms g ; :: thesis: rng (NDentry (g,X,d)) c= ND (V,A)
set f = NDdataSeq (g,X,d);
set D = NDentry (g,X,d);
A3: dom (NDdataSeq (g,X,d)) = dom X by Def4;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (NDentry (g,X,d)) or y in ND (V,A) )
assume y in rng (NDentry (g,X,d)) ; :: thesis: y in ND (V,A)
then consider a being object such that
A4: a in dom (NDentry (g,X,d)) and
A5: (NDentry (g,X,d)) . a = y by FUNCT_1:def 3;
[a,y] in NDentry (g,X,d) by A4, A5, FUNCT_1:1;
then consider v being object such that
A6: v in dom (NDdataSeq (g,X,d)) and
A7: (NDdataSeq (g,X,d)) . v = [a,y] by FUNCT_1:def 3;
reconsider v = v as Element of NAT by A6;
(NDdataSeq (g,X,d)) . v = [(X . v),((g . v) . d)] by A3, A6, Def4;
then A8: y = (g . v) . d by A7, XTUPLE_0:1;
( 1 <= v & v <= len g ) by A1, A3, A6, FINSEQ_3:25;
then g . v is SCBinominativeFunction of V,A by Def6;
then A9: rng (g . v) c= ND (V,A) by RELAT_1:def 19;
d in dom (g . v) by A1, A3, A6, A2;
hence y in ND (V,A) by A8, A9, FUNCT_1:3; :: thesis: verum