let V, A be set ; :: thesis: <*(NDSS (V,A))*> IsNDRankSeq V,A
set S = <*(NDSS (V,A))*>;
thus <*(NDSS (V,A))*> . 1 = NDSS (V,A) ; :: according to NOMIN_1:def 4 :: thesis: for n being Nat st n in dom <*(NDSS (V,A))*> & n + 1 in dom <*(NDSS (V,A))*> holds
<*(NDSS (V,A))*> . (n + 1) = NDSS (V,(A \/ (<*(NDSS (V,A))*> . n)))
let n be Nat; :: thesis: ( n in dom <*(NDSS (V,A))*> & n + 1 in dom <*(NDSS (V,A))*> implies <*(NDSS (V,A))*> . (n + 1) = NDSS (V,(A \/ (<*(NDSS (V,A))*> . n))) )
assume A1: ( n in dom <*(NDSS (V,A))*> & n + 1 in dom <*(NDSS (V,A))*> ) ; :: thesis: <*(NDSS (V,A))*> . (n + 1) = NDSS (V,(A \/ (<*(NDSS (V,A))*> . n)))
dom <*(NDSS (V,A))*> = {1} by FINSEQ_1:2, FINSEQ_1:def 8;
then ( n = 1 & n + 1 = 1 ) by A1, TARSKI:def 1;
hence <*(NDSS (V,A))*> . (n + 1) = NDSS (V,(A \/ (<*(NDSS (V,A))*> . n))) ; :: thesis: verum