let a be object ; :: thesis: for V, A being set
for f being b₁ -valued FinSequence st len f > 0 holds
naming (V,A,f,a) is NonatomicND of V,A
let V, A be set ; :: thesis: for f being V -valued FinSequence st len f > 0 holds
naming (V,A,f,a) is NonatomicND of V,A
let f be V -valued FinSequence; :: thesis: ( len f > 0 implies naming (V,A,f,a) is NonatomicND of V,A )
assume A1: len f > 0 ; :: thesis: naming (V,A,f,a) is NonatomicND of V,A
A2: len (namingSeq (V,A,f,a)) = len f by A1, Def14;
then 0 + 1 <= len (namingSeq (V,A,f,a)) by A1, NAT_1:13;
hence naming (V,A,f,a) is NonatomicND of V,A by A2, Th58; :: thesis: verum