let V, A be set ; :: thesis: for S, S1 being FinSequence st S IsNDRankSeq V,A & S1 c= S & S1 <> {} holds

S1 IsNDRankSeq V,A

let S, S1 be FinSequence; :: thesis: ( S IsNDRankSeq V,A & S1 c= S & S1 <> {} implies S1 IsNDRankSeq V,A )

assume that

A1: S IsNDRankSeq V,A and

A2: S1 c= S and

A3: S1 <> {} ; :: thesis: S1 IsNDRankSeq V,A

A4: dom S1 c= dom S by A2, XTUPLE_0:8;

rng S1 <> {} by A3;

then 1 in dom S1 by FINSEQ_3:32;

hence S1 . 1 = NDSS (V,A) by A1, A2, GRFUNC_1:2; :: according to NOMIN_1:def 4 :: thesis: for n being Nat st n in dom S1 & n + 1 in dom S1 holds

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

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

assume that

A5: n in dom S1 and

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

S1 . n = S . n by A2, A5, GRFUNC_1:2;

hence NDSS (V,(A \/ (S1 . n))) = S . (n + 1) by A1, A4, A5, A6

.= S1 . (n + 1) by A2, A6, GRFUNC_1:2 ;

:: thesis: verum

S1 IsNDRankSeq V,A

let S, S1 be FinSequence; :: thesis: ( S IsNDRankSeq V,A & S1 c= S & S1 <> {} implies S1 IsNDRankSeq V,A )

assume that

A1: S IsNDRankSeq V,A and

A2: S1 c= S and

A3: S1 <> {} ; :: thesis: S1 IsNDRankSeq V,A

A4: dom S1 c= dom S by A2, XTUPLE_0:8;

rng S1 <> {} by A3;

then 1 in dom S1 by FINSEQ_3:32;

hence S1 . 1 = NDSS (V,A) by A1, A2, GRFUNC_1:2; :: according to NOMIN_1:def 4 :: thesis: for n being Nat st n in dom S1 & n + 1 in dom S1 holds

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

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

assume that

A5: n in dom S1 and

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

S1 . n = S . n by A2, A5, GRFUNC_1:2;

hence NDSS (V,(A \/ (S1 . n))) = S . (n + 1) by A1, A4, A5, A6

.= S1 . (n + 1) by A2, A6, GRFUNC_1:2 ;

:: thesis: verum