theorem Th21: :: FINSEQ_6:147

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