let V, A be set ; :: thesis: for n being Nat st 1 <= n holds
(FNDSC (V,A)) | (Seg n) IsNDRankSeq V,A
let n be Nat; :: thesis: ( 1 <= n implies (FNDSC (V,A)) | (Seg n) IsNDRankSeq V,A )
set F = FNDSC (V,A);
set S = (FNDSC (V,A)) | (Seg n);
dom (FNDSC (V,A)) = NAT by Def3;
then A1: dom ((FNDSC (V,A)) | (Seg n)) = Seg n by RELAT_1:62;
assume 1 <= n ; :: thesis: (FNDSC (V,A)) | (Seg n) IsNDRankSeq V,A
then 1 in Seg n ;
hence ((FNDSC (V,A)) | (Seg n)) . 1 = (FNDSC (V,A)) . 1 by FUNCT_1:49
.= NDSS (V,A) by Th9 ;
:: according to NOMIN_1:def 4 :: thesis: for n being Nat st n in dom ((FNDSC (V,A)) | (Seg n)) & n + 1 in dom ((FNDSC (V,A)) | (Seg n)) holds
((FNDSC (V,A)) | (Seg n)) . (n + 1) = NDSS (V,(A \/ (((FNDSC (V,A)) | (Seg n)) . n)))
let n be Nat; :: thesis: ( n in dom ((FNDSC (V,A)) | (Seg n)) & n + 1 in dom ((FNDSC (V,A)) | (Seg n)) implies ((FNDSC (V,A)) | (Seg n)) . (n + 1) = NDSS (V,(A \/ (((FNDSC (V,A)) | (Seg n)) . n))) )
assume A2: n in dom ((FNDSC (V,A)) | (Seg n)) ; :: thesis: ( not n + 1 in dom ((FNDSC (V,A)) | (Seg n)) or ((FNDSC (V,A)) | (Seg n)) . (n + 1) = NDSS (V,(A \/ (((FNDSC (V,A)) | (Seg n)) . n))) )
assume n + 1 in dom ((FNDSC (V,A)) | (Seg n)) ; :: thesis: ((FNDSC (V,A)) | (Seg n)) . (n + 1) = NDSS (V,(A \/ (((FNDSC (V,A)) | (Seg n)) . n)))
hence ((FNDSC (V,A)) | (Seg n)) . (n + 1) = (FNDSC (V,A)) . (n + 1) by A1, FUNCT_1:49
.= NDSS (V,(A \/ ((FNDSC (V,A)) . n))) by Def3
.= NDSS (V,(A \/ (((FNDSC (V,A)) | (Seg n)) . n))) by A1, A2, FUNCT_1:49 ;
:: thesis: verum