let s, t be FinSequence of NAT ; :: thesis: ( 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 ) ; :: thesis: ( 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 ) ; :: thesis: 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

proof

let i be object ; :: thesis: ( i in dom s implies s . i = t . i )
assume i in dom s ; :: thesis: s . i = t . i
then not not i = 1 & ... & not i = 16 by A2, FINSEQ_1:91;
hence s . i = t . i by A1, A3; :: thesis: verum

end;

hence s = t by A4; :: thesis: verum