for a1, a2 being TwoValued Alternating FinSequence st a1 <> a2 & len a1 = len a2 & rng a1 = rng a2 holds
for a being TwoValued Alternating FinSequence st len a = len a1 & rng a = rng a1 & not a = a1 holds
a = a2