let V, A be set ; for S being FinSequence st S IsNDRankSeq V,A holds
S = (FNDSC (V,A)) | (dom S)
let S be FinSequence; ( S IsNDRankSeq V,A implies S = (FNDSC (V,A)) | (dom S) )
assume A1:
S IsNDRankSeq V,A
; 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; FUNCT_1:def 11 for b1 being object holds
( not b1 in dom S or S . b1 = ((FNDSC (V,A)) | (dom S)) . b1 )
let x be object ; ( not x in dom S or S . x = ((FNDSC (V,A)) | (dom S)) . x )
assume A2:
x in dom S
; 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
; verum