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 S_{1}[ Nat] means ( 1 <= $1 & $1 <= len a1 implies a1 . $1 <> a2 . $1 );

A4: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
;

thus for i being Nat holds S_{1}[i]
from NAT_1:sch 2(A16, A4); :: thesis: verum

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 S

A4: for k being Nat st S

S

proof

A16:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A5: ( 1 <= k & k <= len a1 implies a1 . k <> a2 . k ) ; :: thesis: S_{1}[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;

end;assume A5: ( 1 <= k & k <= len a1 implies a1 . k <> a2 . k ) ; :: thesis: S

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;

end;

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

k <= len a1
by A8, NAT_1:13;

then A11: k in dom a1 by A10, FINSEQ_3:25;

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 A9, FUNCT_1:def 3;

then A14: ( a1 . (k + 1) = X or a1 . (k + 1) = Y ) by A13, TARSKI:def 2;

dom a1 = Seg (len a1) by FINSEQ_1:def 3;

then a2 . k in rng a2 by A2, A11, A12, FUNCT_1:def 3;

then A15: ( a2 . k = X or a2 . k = Y ) by A3, A13, TARSKI:def 2;

a1 . k in rng a1 by A11, FUNCT_1:def 3;

then ( a1 . k = X or a1 . k = Y ) by A13, TARSKI:def 2;

hence a1 . (k + 1) <> a2 . (k + 1) by A2, A5, A8, A10, A15, A14, Def4, NAT_1:13; :: thesis: verum

end;then A11: k in dom a1 by A10, FINSEQ_3:25;

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 A9, FUNCT_1:def 3;

then A14: ( a1 . (k + 1) = X or a1 . (k + 1) = Y ) by A13, TARSKI:def 2;

dom a1 = Seg (len a1) by FINSEQ_1:def 3;

then a2 . k in rng a2 by A2, A11, A12, FUNCT_1:def 3;

then A15: ( a2 . k = X or a2 . k = Y ) by A3, A13, TARSKI:def 2;

a1 . k in rng a1 by A11, FUNCT_1:def 3;

then ( a1 . k = X or a1 . k = Y ) by A13, TARSKI:def 2;

hence a1 . (k + 1) <> a2 . (k + 1) by A2, A5, A8, A10, A15, A14, Def4, NAT_1:13; :: thesis: verum

thus for i being Nat holds S