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₁( 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₁(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 FINSEQ_3:103;
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 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;

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

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

then (<*A*> ^ F) . (n + 1) = S . n by A8, A12, A1, FINSEQ_3:25, FINSEQ_3:103;
hence NDSS (V,(A \/ (S . n))) = S . (n + 1) by A3, A10; :: thesis: verum

end;

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, FINSEQ_3:103, 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;

end;

end;

thus for n being Nat st n in dom S holds
S . n = NDSS (V,(A \/ ((<*A*> ^ F) . n))) by A3; :: thesis: verum