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-Right (r,120))*>;
( 8 <= 128 - 8 & 8 <= 128 - 16 & 8 <= 128 - 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 <= 128 - 32 & 8 <= 128 - 40 & 8 <= 128 - 48 & 8 <= 128 - 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 <= 128 - 64 & 8 <= 128 - 72 & 8 <= 128 - 80 & 8 <= 128 - 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 <= 128 - 96 & 8 <= 128 - 104 & 8 <= 128 - 112 & 8 = 128 - 120 & 104 = 96 + 8 & 112 = 96 + 16 & 120 = 96 + 24 & 8 = 128 - 120 )
;
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-Right (r,120))*> as Element of 4 -tuples_on (8 -tuples_on BOOLEAN) by Lm3;
set T1 = <*R1,R2*>;
set T2 = <*R3,R4*>;
set T = <*R1,R2*> ^ <*R3,R4*>;
A4:
(<*R1,R2*> ^ <*R3,R4*>) . 1 = <*R1,R2*> . 1 & ... & (<*R1,R2*> ^ <*R3,R4*>) . 2 = <*R1,R2*> . 2
by FINSEQ_3:154;
A5:
(<*R1,R2*> ^ <*R3,R4*>) . (2 + 1) = <*R3,R4*> . 1 & ... & (<*R1,R2*> ^ <*R3,R4*>) . (2 + 2) = <*R3,R4*> . 2
by FINSEQ_3:155;
( len (<*R1,R2*> ^ <*R3,R4*>) = 4 & <*R1,R2*> ^ <*R3,R4*> is FinSequence of 4 -tuples_on (8 -tuples_on BOOLEAN) )
by CARD_1:def 7;
then reconsider T = <*R1,R2*> ^ <*R3,R4*> as Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) by FINSEQ_2:92;
take
T
; ( 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-Right (r,120))*> )
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-Right (r,120))*> )
by A4, A5, FINSEQ_1:44; verum