let a be object ; :: thesis: for V, A being set

for f being b_{1} -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

for f being b

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