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

for n being Nat

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

for n being Nat

for f being b

(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;

end;

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;hence (namingSeq (V,A,f,a)) . n is NonatomicND of V,A ; :: thesis: verum

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;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