let a1, a2 be TwoValued Alternating FinSequence; ( 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
; a1 = a2
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;
( S1[k] implies S1[k + 1] )
assume A5:
( 1
<= k &
k <= len a1 implies
a1 . k = a2 . k )
;
S1[k + 1]
A6:
(
0 = k or (
0 < k &
0 + 1
= 1 ) )
;
assume that A7:
1
<= k + 1
and A8:
k + 1
<= len a1
;
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 A10:
1
<= k
;
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;
verum end; end;
end;
A15:
S1[ 0 ]
;
for i being Nat holds S1[i]
from NAT_1:sch 2(A15, A4);
hence
a1 = a2
by A1; verum