let a1, a2 be TwoValued Alternating FinSequence; ( 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
; 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; ( 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
; ( a = a1 or a = a2 )
assume A6:
a <> a1
; a = a2
now for i being Nat st 1 <= i & i <= len a holds
a . i = a2 . ilet i be
Nat;
( 1 <= i & i <= len a implies a . i = a2 . i )assume that A7:
1
<= i
and A8:
i <= len a
;
a . i = a2 . iconsider X,
Y being
object 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, A11, A13, Th21;
verum end;
hence
a = a2
by A2, A4; verum