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