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 being Element of S ex s being FinSequence of S st
( s is 56 -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 )
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 be Element of S; ex s being FinSequence of S st
( s is 56 -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 )
consider a1 being FinSequence of S such that
A1:
( a1 is 48 -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 & a1 . 33 = x33 & a1 . 34 = x34 & a1 . 35 = x35 & a1 . 36 = x36 & a1 . 37 = x37 & a1 . 38 = x38 & a1 . 39 = x39 & a1 . 40 = x40 & a1 . 41 = x41 & a1 . 42 = x42 & a1 . 43 = x43 & a1 . 44 = x44 & a1 . 45 = x45 & a1 . 46 = x46 & a1 . 47 = x47 & a1 . 48 = x48 )
by Th23;
consider a2 being FinSequence of S such that
A2:
( a2 is 8 -element & a2 . 1 = x49 & a2 . 2 = x50 & a2 . 3 = x51 & a2 . 4 = x52 & a2 . 5 = x53 & a2 . 6 = x54 & a2 . 7 = x55 & a2 . 8 = x56 )
by Th20;
reconsider a1 = a1 as 48 -element FinSequence of S by A1;
reconsider a2 = a2 as 8 -element FinSequence of S by A2;
take
a1 ^ a2
; ( a1 ^ a2 is 56 -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 )
thus
a1 ^ a2 is 56 -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 )
A3:
(a1 ^ a2) . 1 = a1 . 1 & ... & (a1 ^ a2) . 48 = a1 . 48
by FINSEQ_3:154;
(a1 ^ a2) . (48 + 1) = a2 . 1 & ... & (a1 ^ a2) . (48 + 8) = a2 . 8
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 )
by A3, A1, A2; verum