let V, A be set ; :: thesis: for S being FinSequence st S IsNDRankSeq V,A holds
S = (FNDSC (V,A)) | (dom S)
let S be FinSequence; :: thesis: ( S IsNDRankSeq V,A implies S = (FNDSC (V,A)) | (dom S) )
assume A1: S IsNDRankSeq V,A ; :: thesis: S = (FNDSC (V,A)) | (dom S)
set F = FNDSC (V,A);
set G = (FNDSC (V,A)) | (dom S);
dom (FNDSC (V,A)) = NAT by Def3;
hence dom S = dom ((FNDSC (V,A)) | (dom S)) by RELAT_1:62; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom S or S . b₁ = ((FNDSC (V,A)) | (dom S)) . b₁ )
let x be object ; :: thesis: ( not x in dom S or S . x = ((FNDSC (V,A)) | (dom S)) . x )
assume A2: x in dom S ; :: thesis: S . x = ((FNDSC (V,A)) | (dom S)) . x
thus S . x = (FNDSC (V,A)) . x by A1, A2, Th19
.= ((FNDSC (V,A)) | (dom S)) . x by A2, FUNCT_1:49 ; :: thesis: verum