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