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

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 set such that
X <> Y and
A9: rng a = {X,Y} by Th19;
A10: i in dom a by A7, A8, FINSEQ_3:25;
then a . i in rng a by FUNCT_1:def 3;
then A11: ( a . i = X or a . i = Y ) by A9, TARSKI:def 2;
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 A4, A10, A12, FUNCT_1:def 3;
then A13: ( a1 . i = X or a1 . i = Y ) by A5, A9, TARSKI:def 2;
dom a2 = Seg (len a2) by FINSEQ_1:def 3;
then a2 . i in rng a2 by A2, A4, A10, A12, FUNCT_1:def 3;
then ( a2 . i = X or a2 . i = Y ) by A3, A5, A9, TARSKI:def 2;
hence a . i = a2 . i by A1, A2, A3, A4, A5, A6, A7, A8, A10, A11, A13, Th21; :: thesis: verum

end;

hence a = a2 by A2, A4, FINSEQ_1:14; :: thesis: verum