let V, A be set ; :: thesis: for F being FinSequence st F IsNDRankSeq V,A holds

ex S being FinSequence st

( len S = 1 + (len F) & S IsNDRankSeq V,A & ( for n being Nat st n in dom S holds

S . n = NDSS (V,(A \/ ((<*A*> ^ F) . n))) ) )

let F be FinSequence; :: thesis: ( F IsNDRankSeq V,A implies ex S being FinSequence st

( len S = 1 + (len F) & S IsNDRankSeq V,A & ( for n being Nat st n in dom S holds

S . n = NDSS (V,(A \/ ((<*A*> ^ F) . n))) ) ) )

assume A1: F IsNDRankSeq V,A ; :: thesis: ex S being FinSequence st

( len S = 1 + (len F) & S IsNDRankSeq V,A & ( for n being Nat st n in dom S holds

S . n = NDSS (V,(A \/ ((<*A*> ^ F) . n))) ) )

set G = <*A*> ^ F;

deffunc H_{1}( object ) -> set = NDSS (V,(A \/ ((<*A*> ^ F) . $1)));

consider S being FinSequence such that

A2: len S = len (<*A*> ^ F) and

A3: for n being Nat st n in dom S holds

S . n = H_{1}(n)
from FINSEQ_1:sch 2();

take S ; :: thesis: ( len S = 1 + (len F) & S IsNDRankSeq V,A & ( for n being Nat st n in dom S holds

S . n = NDSS (V,(A \/ ((<*A*> ^ F) . n))) ) )

len <*A*> = 1 by FINSEQ_1:39;

hence A4: len S = 1 + (len F) by A2, FINSEQ_1:22; :: thesis: ( S IsNDRankSeq V,A & ( for n being Nat st n in dom S holds

S . n = NDSS (V,(A \/ ((<*A*> ^ F) . n))) ) )

A5: (<*A*> ^ F) . 1 = A by FINSEQ_1:41;

A6: for n being Nat st n in dom F holds

(<*A*> ^ F) . (n + 1) = F . n by Th1;

A7: 1 <= len S by A4, NAT_1:11;

thus S IsNDRankSeq V,A :: thesis: for n being Nat st n in dom S holds

S . n = NDSS (V,(A \/ ((<*A*> ^ F) . n)))

S . n = NDSS (V,(A \/ ((<*A*> ^ F) . n))) by A3; :: thesis: verum

ex S being FinSequence st

( len S = 1 + (len F) & S IsNDRankSeq V,A & ( for n being Nat st n in dom S holds

S . n = NDSS (V,(A \/ ((<*A*> ^ F) . n))) ) )

let F be FinSequence; :: thesis: ( F IsNDRankSeq V,A implies ex S being FinSequence st

( len S = 1 + (len F) & S IsNDRankSeq V,A & ( for n being Nat st n in dom S holds

S . n = NDSS (V,(A \/ ((<*A*> ^ F) . n))) ) ) )

assume A1: F IsNDRankSeq V,A ; :: thesis: ex S being FinSequence st

( len S = 1 + (len F) & S IsNDRankSeq V,A & ( for n being Nat st n in dom S holds

S . n = NDSS (V,(A \/ ((<*A*> ^ F) . n))) ) )

set G = <*A*> ^ F;

deffunc H

consider S being FinSequence such that

A2: len S = len (<*A*> ^ F) and

A3: for n being Nat st n in dom S holds

S . n = H

take S ; :: thesis: ( len S = 1 + (len F) & S IsNDRankSeq V,A & ( for n being Nat st n in dom S holds

S . n = NDSS (V,(A \/ ((<*A*> ^ F) . n))) ) )

len <*A*> = 1 by FINSEQ_1:39;

hence A4: len S = 1 + (len F) by A2, FINSEQ_1:22; :: thesis: ( S IsNDRankSeq V,A & ( for n being Nat st n in dom S holds

S . n = NDSS (V,(A \/ ((<*A*> ^ F) . n))) ) )

A5: (<*A*> ^ F) . 1 = A by FINSEQ_1:41;

A6: for n being Nat st n in dom F holds

(<*A*> ^ F) . (n + 1) = F . n by Th1;

A7: 1 <= len S by A4, NAT_1:11;

thus S IsNDRankSeq V,A :: thesis: for n being Nat st n in dom S holds

S . n = NDSS (V,(A \/ ((<*A*> ^ F) . n)))

proof

thus
for n being Nat st n in dom S holds
thus A8: S . 1 =
NDSS (V,(A \/ ((<*A*> ^ F) . 1)))
by A3, A7, FINSEQ_3:25

.= NDSS (V,A) by A5 ; :: according to NOMIN_1:def 4 :: thesis: for n being Nat st n in dom S & n + 1 in dom S holds

S . (n + 1) = NDSS (V,(A \/ (S . n)))

let n be Nat; :: thesis: ( n in dom S & n + 1 in dom S implies S . (n + 1) = NDSS (V,(A \/ (S . n))) )

assume that

A9: n in dom S and

A10: n + 1 in dom S ; :: thesis: S . (n + 1) = NDSS (V,(A \/ (S . n)))

A11: 1 <= n by A9, FINSEQ_3:25;

A12: n <= len F by A4, A10, FINSEQ_3:25, XREAL_1:6;

then A13: n in dom F by A11, FINSEQ_3:25;

end;.= NDSS (V,A) by A5 ; :: according to NOMIN_1:def 4 :: thesis: for n being Nat st n in dom S & n + 1 in dom S holds

S . (n + 1) = NDSS (V,(A \/ (S . n)))

let n be Nat; :: thesis: ( n in dom S & n + 1 in dom S implies S . (n + 1) = NDSS (V,(A \/ (S . n))) )

assume that

A9: n in dom S and

A10: n + 1 in dom S ; :: thesis: S . (n + 1) = NDSS (V,(A \/ (S . n)))

A11: 1 <= n by A9, FINSEQ_3:25;

A12: n <= len F by A4, A10, FINSEQ_3:25, XREAL_1:6;

then A13: n in dom F by A11, FINSEQ_3:25;

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

end;

suppose
n = 1
; :: thesis: S . (n + 1) = NDSS (V,(A \/ (S . n)))

then
(<*A*> ^ F) . (n + 1) = S . n
by A8, A12, A1, Th1, FINSEQ_3:25;

hence NDSS (V,(A \/ (S . n))) = S . (n + 1) by A3, A10; :: thesis: verum

end;hence NDSS (V,(A \/ (S . n))) = S . (n + 1) by A3, A10; :: thesis: verum

suppose A14:
n > 1
; :: thesis: S . (n + 1) = NDSS (V,(A \/ (S . n)))

then reconsider m = n - 1 as Element of NAT by INT_1:5;

S . n = NDSS (V,(A \/ ((<*A*> ^ F) . (m + 1)))) by A3, A9

.= NDSS (V,(A \/ (F . m))) by A13, A14, Th1, CGAMES_1:20

.= F . (m + 1) by A1, A13, A14, CGAMES_1:20 ;

then (<*A*> ^ F) . (n + 1) = S . n by A6, A12, A11, FINSEQ_3:25;

hence NDSS (V,(A \/ (S . n))) = S . (n + 1) by A3, A10; :: thesis: verum

end;S . n = NDSS (V,(A \/ ((<*A*> ^ F) . (m + 1)))) by A3, A9

.= NDSS (V,(A \/ (F . m))) by A13, A14, Th1, CGAMES_1:20

.= F . (m + 1) by A1, A13, A14, CGAMES_1:20 ;

then (<*A*> ^ F) . (n + 1) = S . n by A6, A12, A11, FINSEQ_3:25;

hence NDSS (V,(A \/ (S . n))) = S . (n + 1) by A3, A10; :: thesis: verum

S . n = NDSS (V,(A \/ ((<*A*> ^ F) . n))) by A3; :: thesis: verum