let S be non empty set ; :: thesis: for x1, x2, x3, x4, x5, x6, x7, x8 being Element of S ex s being FinSequence of S st
( s is 8 -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 )
let x1, x2, x3, x4, x5, x6, x7, x8 be Element of S; :: thesis: ex s being FinSequence of S st
( s is 8 -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 )
set a1 = <*x1,x2,x3,x4*>;
set a2 = <*x5,x6,x7,x8*>;
take b1 = <*x1,x2,x3,x4*> ^ <*x5,x6,x7,x8*>; :: thesis: ( b1 is 8 -element & b1 . 1 = x1 & b1 . 2 = x2 & b1 . 3 = x3 & b1 . 4 = x4 & b1 . 5 = x5 & b1 . 6 = x6 & b1 . 7 = x7 & b1 . 8 = x8 )
A1: b1 . 1 = <*x1,x2,x3,x4*> . 1 & ... & b1 . 4 = <*x1,x2,x3,x4*> . 4 by FINSEQ_3:154;
b1 . (4 + 1) = <*x5,x6,x7,x8*> . 1 & ... & b1 . (4 + 4) = <*x5,x6,x7,x8*> . 4 by FINSEQ_3:155;
hence ( b1 is 8 -element & b1 . 1 = x1 & b1 . 2 = x2 & b1 . 3 = x3 & b1 . 4 = x4 & b1 . 5 = x5 & b1 . 6 = x6 & b1 . 7 = x7 & b1 . 8 = x8 ) by A1; :: thesis: verum