theorem Th20: :: FINSEQ_6:146

for a1, a2 being TwoValued Alternating FinSequence st len a1 = len a2 & rng a1 = rng a2 & a1 . 1 = a2 . 1 holds
a1 = a2