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

assume that
A1: a1 <> a2 and
A2: len a1 = len a2 and
A3: rng a1 = rng a2 ; :: thesis: for i being Nat st 1 <= i & i <= len a1 holds
a1 . i <> a2 . i

defpred S1[ Nat] means ( 1 <= \$1 & \$1 <= len a1 implies a1 . \$1 <> a2 . \$1 );
A4: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A5: ( 1 <= k & k <= len a1 implies a1 . k <> a2 . k ) ; :: thesis: S1[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 ;
per cases ( 0 = k or 1 <= k ) by ;
suppose 0 = k ; :: thesis: a1 . (k + 1) <> a2 . (k + 1)
hence a1 . (k + 1) <> a2 . (k + 1) by A1, A2, A3, Th20; :: thesis: verum
end;
suppose A10: 1 <= k ; :: thesis: a1 . (k + 1) <> a2 . (k + 1)
k <= len a1 by ;
then A11: k in dom a1 by ;
A12: dom a2 = Seg (len a2) by FINSEQ_1:def 3;
consider X, Y being object such that
X <> Y and
A13: rng a1 = {X,Y} by Th19;
a1 . (k + 1) in rng a1 by ;
then A14: ( a1 . (k + 1) = X or a1 . (k + 1) = Y ) by ;
dom a1 = Seg (len a1) by FINSEQ_1:def 3;
then a2 . k in rng a2 by ;
then A15: ( a2 . k = X or a2 . k = Y ) by ;
a1 . k in rng a1 by ;
then ( a1 . k = X or a1 . k = Y ) by ;
hence a1 . (k + 1) <> a2 . (k + 1) by A2, A5, A8, A10, A15, A14, Def4, NAT_1:13; :: thesis: verum
end;
end;
end;
A16: S1[ 0 ] ;
thus for i being Nat holds S1[i] from NAT_1:sch 2(A16, A4); :: thesis: verum