let a1, a2 be TwoValued Alternating FinSequence; :: thesis: ( a1 <> a2 & len a1 = len a2 & rng a1 = rng a2 implies for a being TwoValued Alternating FinSequence st len a = len a1 & rng a = rng a1 & not a = a1 holds
a = a2 )

assume that
A1: a1 <> a2 and
A2: len a1 = len a2 and
A3: rng a1 = rng a2 ; :: thesis: for a being TwoValued Alternating FinSequence st len a = len a1 & rng a = rng a1 & not a = a1 holds
a = a2

let a be TwoValued Alternating FinSequence; :: thesis: ( len a = len a1 & rng a = rng a1 & not a = a1 implies a = a2 )
assume that
A4: len a = len a1 and
A5: rng a = rng a1 ; :: thesis: ( a = a1 or a = a2 )
assume A6: a <> a1 ; :: thesis: a = a2
now :: thesis: for i being Nat st 1 <= i & i <= len a holds
a . i = a2 . i
let i be Nat; :: thesis: ( 1 <= i & i <= len a implies a . i = a2 . i )
assume that
A7: 1 <= i and
A8: i <= len a ; :: thesis: a . i = a2 . i
consider X, Y being object such that
X <> Y and
A9: rng a = {X,Y} by Th19;
A10: i in dom a by ;
then a . i in rng a by FUNCT_1:def 3;
then A11: ( a . i = X or a . i = Y ) by ;
A12: dom a = Seg (len a) by FINSEQ_1:def 3;
dom a1 = Seg (len a1) by FINSEQ_1:def 3;
then a1 . i in rng a1 by ;
then A13: ( a1 . i = X or a1 . i = Y ) by ;
dom a2 = Seg (len a2) by FINSEQ_1:def 3;
then a2 . i in rng a2 by ;
then ( a2 . i = X or a2 . i = Y ) by ;
hence a . i = a2 . i by A1, A2, A3, A4, A5, A6, A7, A8, A11, A13, Th21; :: thesis: verum
end;
hence a = a2 by A2, A4; :: thesis: verum