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