let S be non empty set ; for x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16 being Element of S ex s being FinSequence of S st
( s is 16 -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 )
let x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16 be Element of S; ex s being FinSequence of S st
( s is 16 -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 )
consider a1 being FinSequence of S such that
A1:
( a1 is 8 -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 )
by Th20;
consider a2 being FinSequence of S such that
A2:
( a2 is 8 -element & a2 . 1 = x9 & a2 . 2 = x10 & a2 . 3 = x11 & a2 . 4 = x12 & a2 . 5 = x13 & a2 . 6 = x14 & a2 . 7 = x15 & a2 . 8 = x16 )
by Th20;
reconsider a1 = a1, a2 = a2 as 8 -element FinSequence of S by A1, A2;
take
a1 ^ a2
; ( a1 ^ a2 is 16 -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 )
thus
a1 ^ a2 is 16 -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 )
A3:
(a1 ^ a2) . 1 = a1 . 1 & ... & (a1 ^ a2) . 8 = a1 . 8
by FINSEQ_3:154;
(a1 ^ a2) . (8 + 1) = a2 . 1 & ... & (a1 ^ a2) . (8 + 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 )
by A3, A1, A2; verum