let a1, a2 be TwoValued Alternating FinSequence; :: thesis: ( len a1 = len a2 & rng a1 = rng a2 & a1 . 1 = a2 . 1 implies a1 = a2 )
assume that
A1: len a1 = len a2 and
A2: rng a1 = rng a2 and
A3: a1 . 1 = a2 . 1 ; :: thesis: a1 = a2
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= len a1 implies a1 . $1 = a2 . $1 );
A4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: ( 1 <= k & k <= len a1 implies a1 . k = a2 . k ) ; :: thesis: S₁[k + 1]
A6: ( 0 = k or ( 0 < k & 0 + 1 = 1 ) ) ;
assume that
A7: 1 <= k + 1 and
A8: k + 1 <= len a1 ; :: thesis: a1 . (k + 1) = a2 . (k + 1)
A9: k + 1 in dom a1 by A7, A8, FINSEQ_3:25;

per cases ( 0 = k or 1 <= k ) by A6, NAT_1:13;

suppose 0 = k ; :: thesis: a1 . (k + 1) = a2 . (k + 1)

hence a1 . (k + 1) = a2 . (k + 1) by A3; :: thesis: verum

end;

suppose A10: 1 <= k ; :: thesis: a1 . (k + 1) = a2 . (k + 1)

A11: dom a2 = Seg (len a2) by FINSEQ_1:def 3;
consider X, Y being object such that
X <> Y and
A12: rng a1 = {X,Y} by Th19;
a1 . (k + 1) in rng a1 by A9, FUNCT_1:def 3;
then A13: ( a1 . (k + 1) = X or a1 . (k + 1) = Y ) by A12, TARSKI:def 2;
dom a1 = Seg (len a1) by FINSEQ_1:def 3;
then a2 . (k + 1) in rng a2 by A1, A9, A11, FUNCT_1:def 3;
then A14: ( a2 . (k + 1) = X or a2 . (k + 1) = Y ) by A2, A12, TARSKI:def 2;
k <= len a1 by A8, NAT_1:13;
then k in dom a1 by A10, FINSEQ_3:25;
then a1 . k in rng a1 by FUNCT_1:def 3;
then ( a1 . k = X or a1 . k = Y ) by A12, TARSKI:def 2;
hence a1 . (k + 1) = a2 . (k + 1) by A1, A5, A8, A10, A13, A14, Def4, NAT_1:13; :: thesis: verum

end;

end;

end;

A15: S₁[ 0 ] ;
for i being Nat holds S₁[i] from NAT_1:sch 2(A15, A4);
hence a1 = a2 by A1; :: thesis: verum