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 being Element of S ex s being FinSequence of S st
( s is 32 -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 )
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 be Element of S; ex s being FinSequence of S st
( s is 32 -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 )
consider a1 being FinSequence of S such that
A1:
( a1 is 16 -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 )
by Th21;
consider a2 being FinSequence of S such that
A2:
( a2 is 16 -element & a2 . 1 = x17 & a2 . 2 = x18 & a2 . 3 = x19 & a2 . 4 = x20 & a2 . 5 = x21 & a2 . 6 = x22 & a2 . 7 = x23 & a2 . 8 = x24 & a2 . 9 = x25 & a2 . 10 = x26 & a2 . 11 = x27 & a2 . 12 = x28 & a2 . 13 = x29 & a2 . 14 = x30 & a2 . 15 = x31 & a2 . 16 = x32 )
by Th21;
reconsider a1 = a1, a2 = a2 as 16 -element FinSequence of S by A1, A2;
take
a1 ^ a2
; ( a1 ^ a2 is 32 -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 )
thus
a1 ^ a2 is 32 -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 )
A3:
(a1 ^ a2) . 1 = a1 . 1 & ... & (a1 ^ a2) . 16 = a1 . 16
by FINSEQ_3:154;
(a1 ^ a2) . (16 + 1) = a2 . 1 & ... & (a1 ^ a2) . (16 + 16) = a2 . 16
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 )
by A3, A1, A2; verum