set R1 = <*(Op-Left (r,8)),(Op-Left ((Op-Right (r,8)),8)),(Op-Left ((Op-Right (r,16)),8)),(Op-Left ((Op-Right (r,24)),8))*>;
set R2 = <*(Op-Left ((Op-Right (r,32)),8)),(Op-Left ((Op-Right (r,40)),8)),(Op-Left ((Op-Right (r,48)),8)),(Op-Left ((Op-Right (r,56)),8))*>;
set R3 = <*(Op-Left ((Op-Right (r,64)),8)),(Op-Left ((Op-Right (r,72)),8)),(Op-Left ((Op-Right (r,80)),8)),(Op-Left ((Op-Right (r,88)),8))*>;
set R4 = <*(Op-Left ((Op-Right (r,96)),8)),(Op-Left ((Op-Right (r,104)),8)),(Op-Left ((Op-Right (r,112)),8)),(Op-Left ((Op-Right (r,120)),8))*>;
set R5 = <*(Op-Left ((Op-Right (r,128)),8)),(Op-Left ((Op-Right (r,136)),8)),(Op-Left ((Op-Right (r,144)),8)),(Op-Left ((Op-Right (r,152)),8))*>;
set R6 = <*(Op-Left ((Op-Right (r,160)),8)),(Op-Left ((Op-Right (r,168)),8)),(Op-Left ((Op-Right (r,176)),8)),(Op-Right (r,184))*>;
( 8 <= 192 - 8 & 8 <= 192 - 16 & 8 <= 192 - 24 ) ;
then reconsider R1 = <*(Op-Left (r,8)),(Op-Left ((Op-Right (r,8)),8)),(Op-Left ((Op-Right (r,16)),8)),(Op-Left ((Op-Right (r,24)),8))*> as Element of 4 -tuples_on (8 -tuples_on BOOLEAN) by Lm1;
( 8 <= 192 - 32 & 8 <= 192 - 40 & 8 <= 192 - 48 & 8 <= 192 - 56 & 40 = 32 + 8 & 48 = 32 + 16 & 56 = 32 + 24 ) ;
then reconsider R2 = <*(Op-Left ((Op-Right (r,32)),8)),(Op-Left ((Op-Right (r,40)),8)),(Op-Left ((Op-Right (r,48)),8)),(Op-Left ((Op-Right (r,56)),8))*> as Element of 4 -tuples_on (8 -tuples_on BOOLEAN) by Lm2;
( 8 <= 192 - 64 & 8 <= 192 - 72 & 8 <= 192 - 80 & 8 <= 192 - 88 & 72 = 64 + 8 & 80 = 64 + 16 & 88 = 64 + 24 ) ;
then reconsider R3 = <*(Op-Left ((Op-Right (r,64)),8)),(Op-Left ((Op-Right (r,72)),8)),(Op-Left ((Op-Right (r,80)),8)),(Op-Left ((Op-Right (r,88)),8))*> as Element of 4 -tuples_on (8 -tuples_on BOOLEAN) by Lm2;
( 8 <= 192 - 96 & 8 <= 192 - 104 & 8 <= 192 - 112 & 8 <= 192 - 120 & 104 = 96 + 8 & 112 = 96 + 16 & 120 = 96 + 24 ) ;
then reconsider R4 = <*(Op-Left ((Op-Right (r,96)),8)),(Op-Left ((Op-Right (r,104)),8)),(Op-Left ((Op-Right (r,112)),8)),(Op-Left ((Op-Right (r,120)),8))*> as Element of 4 -tuples_on (8 -tuples_on BOOLEAN) by Lm2;
( 8 <= 192 - 128 & 8 <= 192 - 136 & 8 <= 192 - 144 & 8 <= 192 - 152 & 136 = 128 + 8 & 144 = 128 + 16 & 152 = 128 + 24 ) ;
then reconsider R5 = <*(Op-Left ((Op-Right (r,128)),8)),(Op-Left ((Op-Right (r,136)),8)),(Op-Left ((Op-Right (r,144)),8)),(Op-Left ((Op-Right (r,152)),8))*> as Element of 4 -tuples_on (8 -tuples_on BOOLEAN) by Lm2;
( 8 <= 192 - 160 & 8 <= 192 - 168 & 8 <= 192 - 176 & 8 = 192 - 184 & 168 = 160 + 8 & 176 = 160 + 16 & 184 = 160 + 24 & 8 = 192 - 184 ) ;
then reconsider R6 = <*(Op-Left ((Op-Right (r,160)),8)),(Op-Left ((Op-Right (r,168)),8)),(Op-Left ((Op-Right (r,176)),8)),(Op-Right (r,184))*> as Element of 4 -tuples_on (8 -tuples_on BOOLEAN) by Lm3;
set T1 = <*R1,R2,R3*>;
set T2 = <*R4,R5,R6*>;
set T = <*R1,R2,R3*> ^ <*R4,R5,R6*>;
A4: (<*R1,R2,R3*> ^ <*R4,R5,R6*>) . 1 = <*R1,R2,R3*> . 1 & ... & (<*R1,R2,R3*> ^ <*R4,R5,R6*>) . 3 = <*R1,R2,R3*> . 3 by FINSEQ_3:154;
A5: (<*R1,R2,R3*> ^ <*R4,R5,R6*>) . (3 + 1) = <*R4,R5,R6*> . 1 & ... & (<*R1,R2,R3*> ^ <*R4,R5,R6*>) . (3 + 3) = <*R4,R5,R6*> . 3 by FINSEQ_3:155;
( len (<*R1,R2,R3*> ^ <*R4,R5,R6*>) = 6 & <*R1,R2,R3*> ^ <*R4,R5,R6*> is FinSequence of 4 -tuples_on (8 -tuples_on BOOLEAN) ) by CARD_1:def 7;
then reconsider T = <*R1,R2,R3*> ^ <*R4,R5,R6*> as Element of 6 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) by FINSEQ_2:92;
take T ; :: thesis:
thus ( T . 1 = <*(Op-Left (r,8)),(Op-Left ((Op-Right (r,8)),8)),(Op-Left ((Op-Right (r,16)),8)),(Op-Left ((Op-Right (r,24)),8))*> & T . 2 = <*(Op-Left ((Op-Right (r,32)),8)),(Op-Left ((Op-Right (r,40)),8)),(Op-Left ((Op-Right (r,48)),8)),(Op-Left ((Op-Right (r,56)),8))*> & T . 3 = <*(Op-Left ((Op-Right (r,64)),8)),(Op-Left ((Op-Right (r,72)),8)),(Op-Left ((Op-Right (r,80)),8)),(Op-Left ((Op-Right (r,88)),8))*> & T . 4 = <*(Op-Left ((Op-Right (r,96)),8)),(Op-Left ((Op-Right (r,104)),8)),(Op-Left ((Op-Right (r,112)),8)),(Op-Left ((Op-Right (r,120)),8))*> & T . 5 = <*(Op-Left ((Op-Right (r,128)),8)),(Op-Left ((Op-Right (r,136)),8)),(Op-Left ((Op-Right (r,144)),8)),(Op-Left ((Op-Right (r,152)),8))*> & T . 6 = <*(Op-Left ((Op-Right (r,160)),8)),(Op-Left ((Op-Right (r,168)),8)),(Op-Left ((Op-Right (r,176)),8)),(Op-Right (r,184))*> ) by A4, A5, FINSEQ_1:45; :: thesis: