theorem Th25:
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,
x33,
x34,
x35,
x36,
x37,
x38,
x39,
x40,
x41,
x42,
x43,
x44,
x45,
x46,
x47,
x48,
x49,
x50,
x51,
x52,
x53,
x54,
x55,
x56,
x57,
x58,
x59,
x60,
x61,
x62,
x63,
x64 being
Element of
S ex
s being
FinSequence of
S st
(
s is 64
-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 &
s . 33
= x33 &
s . 34
= x34 &
s . 35
= x35 &
s . 36
= x36 &
s . 37
= x37 &
s . 38
= x38 &
s . 39
= x39 &
s . 40
= x40 &
s . 41
= x41 &
s . 42
= x42 &
s . 43
= x43 &
s . 44
= x44 &
s . 45
= x45 &
s . 46
= x46 &
s . 47
= x47 &
s . 48
= x48 &
s . 49
= x49 &
s . 50
= x50 &
s . 51
= x51 &
s . 52
= x52 &
s . 53
= x53 &
s . 54
= x54 &
s . 55
= x55 &
s . 56
= x56 &
s . 57
= x57 &
s . 58
= x58 &
s . 59
= x59 &
s . 60
= x60 &
s . 61
= x61 &
s . 62
= x62 &
s . 63
= x63 &
s . 64
= x64 )