theorem Th21:
for
S being non
empty set for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9,
x10,
x11,
x12,
x13,
x14,
x15,
x16 being
Element of
S ex
s being
FinSequence of
S st
(
s is 16
-element &
s . 1
= x1 &
s . 2
= x2 &
s . 3
= x3 &
s . 4
= x4 &
s . 5
= x5 &
s . 6
= x6 &
s . 7
= x7 &
s . 8
= x8 &
s . 9
= x9 &
s . 10
= x10 &
s . 11
= x11 &
s . 12
= x12 &
s . 13
= x13 &
s . 14
= x14 &
s . 15
= x15 &
s . 16
= x16 )