theorem Th23: :: NOMIN_1:23

for V, A being set
for S1, S2 being FinSequence st S1 IsNDRankSeq V,A & S2 IsNDRankSeq V,A & not S1 +* S2 = S1 holds
S1 +* S2 = S2