theorem Th22:
for
S being non
empty set for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9,
x10,
x11,
x12,
x13,
x14,
x15,
x16,
x17,
x18,
x19,
x20,
x21,
x22,
x23,
x24,
x25,
x26,
x27,
x28,
x29,
x30,
x31,
x32 being
Element of
S ex
s being
FinSequence of
S st
(
s is 32
-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 &
s . 17
= x17 &
s . 18
= x18 &
s . 19
= x19 &
s . 20
= x20 &
s . 21
= x21 &
s . 22
= x22 &
s . 23
= x23 &
s . 24
= x24 &
s . 25
= x25 &
s . 26
= x26 &
s . 27
= x27 &
s . 28
= x28 &
s . 29
= x29 &
s . 30
= x30 &
s . 31
= x31 &
s . 32
= x32 )