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 AS1: ( 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 by CARD_1:def 7;
then L1: dom s = Seg 16 by FINSEQ_1:def 3;
assume AS2: ( 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 by CARD_1:def 7;
then L2: dom s = dom t by L1, FINSEQ_1:def 3;
for i being set st i in dom s holds
s . i = t . i

proof

let i be set ; :: thesis: ( i in dom s implies s . i = t . i )
assume i in dom s ; :: thesis: s . i = t . i
then ( i = 1 or i = 2 or i = 3 or i = 4 or i = 5 or i = 6 or i = 7 or i = 8 or i = 9 or i = 10 or i = 11 or i = 12 or i = 13 or i = 14 or i = 15 or i = 16 ) by Lmseg16a, L1;
hence s . i = t . i by AS1, AS2; :: thesis: verum

end;

hence s = t by L2, FUNCT_1:2; :: thesis: verum