theorem Th27:
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
f being
Function of 64,
S st
(
f . 0 = x1 &
f . 1
= x2 &
f . 2
= x3 &
f . 3
= x4 &
f . 4
= x5 &
f . 5
= x6 &
f . 6
= x7 &
f . 7
= x8 &
f . 8
= x9 &
f . 9
= x10 &
f . 10
= x11 &
f . 11
= x12 &
f . 12
= x13 &
f . 13
= x14 &
f . 14
= x15 &
f . 15
= x16 &
f . 16
= x17 &
f . 17
= x18 &
f . 18
= x19 &
f . 19
= x20 &
f . 20
= x21 &
f . 21
= x22 &
f . 22
= x23 &
f . 23
= x24 &
f . 24
= x25 &
f . 25
= x26 &
f . 26
= x27 &
f . 27
= x28 &
f . 28
= x29 &
f . 29
= x30 &
f . 30
= x31 &
f . 31
= x32 &
f . 32
= x33 &
f . 33
= x34 &
f . 34
= x35 &
f . 35
= x36 &
f . 36
= x37 &
f . 37
= x38 &
f . 38
= x39 &
f . 39
= x40 &
f . 40
= x41 &
f . 41
= x42 &
f . 42
= x43 &
f . 43
= x44 &
f . 44
= x45 &
f . 45
= x46 &
f . 46
= x47 &
f . 47
= x48 &
f . 48
= x49 &
f . 49
= x50 &
f . 50
= x51 &
f . 51
= x52 &
f . 52
= x53 &
f . 53
= x54 &
f . 54
= x55 &
f . 55
= x56 &
f . 56
= x57 &
f . 57
= x58 &
f . 58
= x59 &
f . 59
= x60 &
f . 60
= x61 &
f . 61
= x62 &
f . 62
= x63 &
f . 63
= x64 )