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_{1} being object holds

( not b_{1} in dom S or S . b_{1} = ((FNDSC (V,A)) | (dom S)) . b_{1} )

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

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

( not 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