let s, t be FinSequence of NAT ; ( s is 16 -element & s . 1 = 1 & s . 2 = 1 & s . 3 = 2 & s . 4 = 2 & s . 5 = 2 & s . 6 = 2 & s . 7 = 2 & s . 8 = 2 & s . 9 = 1 & s . 10 = 2 & s . 11 = 2 & s . 12 = 2 & s . 13 = 2 & s . 14 = 2 & s . 15 = 2 & s . 16 = 1 & t is 16 -element & t . 1 = 1 & t . 2 = 1 & t . 3 = 2 & t . 4 = 2 & t . 5 = 2 & t . 6 = 2 & t . 7 = 2 & t . 8 = 2 & t . 9 = 1 & t . 10 = 2 & t . 11 = 2 & t . 12 = 2 & t . 13 = 2 & t . 14 = 2 & t . 15 = 2 & t . 16 = 1 implies s = t )
assume A1:
( s is 16 -element & s . 1 = 1 & s . 2 = 1 & s . 3 = 2 & s . 4 = 2 & s . 5 = 2 & s . 6 = 2 & s . 7 = 2 & s . 8 = 2 & s . 9 = 1 & s . 10 = 2 & s . 11 = 2 & s . 12 = 2 & s . 13 = 2 & s . 14 = 2 & s . 15 = 2 & s . 16 = 1 )
; ( not t is 16 -element or not t . 1 = 1 or not t . 2 = 1 or not t . 3 = 2 or not t . 4 = 2 or not t . 5 = 2 or not t . 6 = 2 or not t . 7 = 2 or not t . 8 = 2 or not t . 9 = 1 or not t . 10 = 2 or not t . 11 = 2 or not t . 12 = 2 or not t . 13 = 2 or not t . 14 = 2 or not t . 15 = 2 or not t . 16 = 1 or s = t )
then
len s = 16
;
then A2:
dom s = Seg 16
by FINSEQ_1:def 3;
assume A3:
( t is 16 -element & t . 1 = 1 & t . 2 = 1 & t . 3 = 2 & t . 4 = 2 & t . 5 = 2 & t . 6 = 2 & t . 7 = 2 & t . 8 = 2 & t . 9 = 1 & t . 10 = 2 & t . 11 = 2 & t . 12 = 2 & t . 13 = 2 & t . 14 = 2 & t . 15 = 2 & t . 16 = 1 )
; s = t
then
len t = 16
;
then A4:
dom s = dom t
by A2, FINSEQ_1:def 3;
for i being object st i in dom s holds
s . i = t . i
hence
s = t
by A4; verum