let a1, a2 be TwoValued Alternating FinSequence; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( a = a1 or a = a2 )

assume A6: a <> a1 ; :: thesis: a = a2

a = a2 )

assume that

A1: a1 <> a2 and

A2: len a1 = len a2 and

A3: rng a1 = rng a2 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( a = a1 or a = a2 )

assume A6: a <> a1 ; :: thesis: a = a2

now :: thesis: for i being Nat st 1 <= i & i <= len a holds

a . i = a2 . i

hence
a = a2
by A2, A4; :: thesis: veruma . i = a2 . i

let i be Nat; :: thesis: ( 1 <= i & i <= len a implies a . i = a2 . i )

assume that

A7: 1 <= i and

A8: i <= len a ; :: thesis: a . i = a2 . i

consider 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; :: thesis: verum

end;assume that

A7: 1 <= i and

A8: i <= len a ; :: thesis: a . i = a2 . i

consider 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; :: thesis: verum