let a be object ; :: thesis: for V, A being set
for n being Nat
for f being b₁ -valued FinSequence st 1 <= n & n <= len f holds
(namingSeq (V,A,f,a)) . n is NonatomicND of V,A
let V, A be set ; :: thesis: for n being Nat
for f being V -valued FinSequence st 1 <= n & n <= len f holds
(namingSeq (V,A,f,a)) . n is NonatomicND of V,A
let n be Nat; :: thesis: for f being V -valued FinSequence st 1 <= n & n <= len f holds
(namingSeq (V,A,f,a)) . n is NonatomicND of V,A
let f be V -valued FinSequence; :: thesis: ( 1 <= n & n <= len f implies (namingSeq (V,A,f,a)) . n is NonatomicND of V,A )
assume that
A1: 1 <= n and
A2: n <= len f ; :: thesis: (namingSeq (V,A,f,a)) . n is NonatomicND of V,A
set g = namingSeq (V,A,f,a);

per cases ( n = 1 or n > 1 ) by A1, XXREAL_0:1;

suppose n = 1 ; :: thesis: (namingSeq (V,A,f,a)) . n is NonatomicND of V,A

then (namingSeq (V,A,f,a)) . n = naming (V,A,(f . (len f)),a) by A2, Def14;
hence (namingSeq (V,A,f,a)) . n is NonatomicND of V,A ; :: thesis: verum

end;

suppose A3: n > 1 ; :: thesis: (namingSeq (V,A,f,a)) . n is NonatomicND of V,A

then reconsider k = n - 1 as Element of NAT by INT_1:5;
1 - 1 < k by A3, XREAL_1:9;
then A4: 0 + 1 <= k by INT_1:7;
A5: len f = len (namingSeq (V,A,f,a)) by A1, A2, Def14;
k + 0 < k + 1 by XREAL_1:8;
then k < len (namingSeq (V,A,f,a)) by A2, A5, XXREAL_0:2;
then (namingSeq (V,A,f,a)) . (k + 1) = naming (V,A,(f . ((len f) - k)),((namingSeq (V,A,f,a)) . k)) by A2, A4, Def14;
hence (namingSeq (V,A,f,a)) . n is NonatomicND of V,A ; :: thesis: verum

end;

end;