let V, A be set ; :: thesis: for d being TypeSCNominativeData of V,A
for g being V,A -FPrg-yielding FinSequence
for X being V -valued one-to-one FinSequence st dom g = dom X & d in_doms g holds
NDentry (g,X,d) is NonatomicND of V,A
let d be TypeSCNominativeData of V,A; :: thesis: for g being V,A -FPrg-yielding FinSequence
for X being V -valued one-to-one FinSequence st dom g = dom X & d in_doms g holds
NDentry (g,X,d) is NonatomicND of V,A
let g be V,A -FPrg-yielding FinSequence; :: thesis: for X being V -valued one-to-one FinSequence st dom g = dom X & d in_doms g holds
NDentry (g,X,d) is NonatomicND of V,A
let X be V -valued one-to-one FinSequence; :: thesis: ( dom g = dom X & d in_doms g implies NDentry (g,X,d) is NonatomicND of V,A )
assume A1: ( dom g = dom X & d in_doms g ) ; :: thesis: NDentry (g,X,d) is NonatomicND of V,A
A2: dom (NDentry (g,X,d)) = rng X by Th24;
A3: rng X c= V by RELAT_1:def 19;
rng (NDentry (g,X,d)) c= ND (V,A) by A1, Th30;
hence NDentry (g,X,d) is NonatomicND of V,A by A2, A3, Th6; :: thesis: verum