X0: 0 in BOOLEAN by TARSKI:def 2, MARGREL1:def 11;
X1: 1 in BOOLEAN by TARSKI:def 2, MARGREL1:def 11;
P1: <*0,0,0,0*> is Element of 4 -tuples_on BOOLEAN by LMGSEQ4, X0;
P2: <*0,0,0,1*> is Element of 4 -tuples_on BOOLEAN by LMGSEQ4, X0, X1;
P3: <*0,0,1,0*> is Element of 4 -tuples_on BOOLEAN by LMGSEQ4, X0, X1;
P4: <*0,1,0,0*> is Element of 4 -tuples_on BOOLEAN by LMGSEQ4, X0, X1;
P5: <*1,0,0,0*> is Element of 4 -tuples_on BOOLEAN by LMGSEQ4, X0, X1;
R1: <*1,0,1,1*> is Element of 4 -tuples_on BOOLEAN by LMGSEQ4, X0, X1;
R2: <*0,0,1,1*> is Element of 4 -tuples_on BOOLEAN by LMGSEQ4, X0, X1;
R3: <*0,1,1,0*> is Element of 4 -tuples_on BOOLEAN by LMGSEQ4, X0, X1;
reconsider PP6 = <*(<*0,0,0,0*> ^ <*0,0,0,1*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> as Element of 4 -tuples_on (8 -tuples_on BOOLEAN) by P1, P2, LMGSEQ16;
reconsider PP7 = <*(<*0,0,0,0*> ^ <*0,0,1,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> as Element of 4 -tuples_on (8 -tuples_on BOOLEAN) by P1, P3, LMGSEQ16;
reconsider PP8 = <*(<*0,0,0,0*> ^ <*0,1,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> as Element of 4 -tuples_on (8 -tuples_on BOOLEAN) by P1, P4, LMGSEQ16;
reconsider PP9 = <*(<*0,0,0,0*> ^ <*1,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> as Element of 4 -tuples_on (8 -tuples_on BOOLEAN) by P1, P5, LMGSEQ16;
reconsider PP10 = <*(<*0,0,0,1*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> as Element of 4 -tuples_on (8 -tuples_on BOOLEAN) by P1, P2, LMGSEQ16;
reconsider PP11 = <*(<*0,0,1,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> as Element of 4 -tuples_on (8 -tuples_on BOOLEAN) by P1, P3, LMGSEQ16;
reconsider PP12 = <*(<*0,1,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> as Element of 4 -tuples_on (8 -tuples_on BOOLEAN) by P1, P4, LMGSEQ16;
reconsider PP13 = <*(<*1,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> as Element of 4 -tuples_on (8 -tuples_on BOOLEAN) by P1, P5, LMGSEQ16;
reconsider PP14 = <*(<*0,0,0,1*> ^ <*1,0,1,1*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> as Element of 4 -tuples_on (8 -tuples_on BOOLEAN) by P1, P2, R1, LMGSEQ16;
reconsider PP15 = <*(<*0,0,1,1*> ^ <*0,1,1,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> as Element of 4 -tuples_on (8 -tuples_on BOOLEAN) by P1, R2, R3, LMGSEQ16;
reconsider Q0 = <*PP6,PP7,PP8,PP9,PP10*> as FinSequence ;
reconsider Q1 = <*PP11,PP12,PP13,PP14,PP15*> as FinSequence ;
reconsider IT = Q0 ^ Q1 as Element of 10 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) by LMGSEQ10;
A1: ( len Q0 = 5 & Q0 . 1 = PP6 & Q0 . 2 = PP7 & Q0 . 3 = PP8 & Q0 . 4 = PP9 & Q0 . 5 = PP10 ) by FINSEQ_4:78;
A2: ( len Q1 = 5 & Q1 . 1 = PP11 & Q1 . 2 = PP12 & Q1 . 3 = PP13 & Q1 . 4 = PP14 & Q1 . 5 = PP15 ) by FINSEQ_4:78;
1 in Seg 5 ;
then 1 in dom Q0 by FINSEQ_1:def 3, A1;
then R1: IT . 1 = PP6 by A1, FINSEQ_1:def 7;
2 in Seg 5 ;
then 2 in dom Q0 by FINSEQ_1:def 3, A1;
then R2: IT . 2 = PP7 by A1, FINSEQ_1:def 7;
3 in Seg 5 ;
then 3 in dom Q0 by FINSEQ_1:def 3, A1;
then R3: IT . 3 = PP8 by A1, FINSEQ_1:def 7;
4 in Seg 5 ;
then 4 in dom Q0 by FINSEQ_1:def 3, A1;
then R4: IT . 4 = PP9 by A1, FINSEQ_1:def 7;
5 in Seg 5 ;
then 5 in dom Q0 by FINSEQ_1:def 3, A1;
then R5: IT . 5 = PP10 by A1, FINSEQ_1:def 7;
1 in Seg 5 ;
then 1 in dom Q1 by FINSEQ_1:def 3, A2;
then R10: IT . (5 + 1) = Q1 . 1 by A1, FINSEQ_1:def 7
.= PP11 by FINSEQ_4:78 ;
2 in Seg 5 ;
then 2 in dom Q1 by FINSEQ_1:def 3, A2;
then R20: IT . (5 + 2) = Q1 . 2 by A1, FINSEQ_1:def 7
.= PP12 by FINSEQ_4:78 ;
3 in Seg 5 ;
then 3 in dom Q1 by FINSEQ_1:def 3, A2;
then R30: IT . (5 + 3) = Q1 . 3 by A1, FINSEQ_1:def 7
.= PP13 by FINSEQ_4:78 ;
4 in Seg 5 ;
then 4 in dom Q1 by FINSEQ_1:def 3, A2;
then R40: IT . (5 + 4) = Q1 . 4 by A1, FINSEQ_1:def 7
.= PP14 by FINSEQ_4:78 ;
5 in Seg 5 ;
then 5 in dom Q1 by FINSEQ_1:def 3, A2;
then R50: IT . (5 + 5) = Q1 . 5 by A1, FINSEQ_1:def 7
.= PP15 by FINSEQ_4:78 ;
thus ex b₁ being Element of 10 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( b₁ . 1 = <*(<*0,0,0,0*> ^ <*0,0,0,1*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b₁ . 2 = <*(<*0,0,0,0*> ^ <*0,0,1,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b₁ . 3 = <*(<*0,0,0,0*> ^ <*0,1,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b₁ . 4 = <*(<*0,0,0,0*> ^ <*1,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b₁ . 5 = <*(<*0,0,0,1*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b₁ . 6 = <*(<*0,0,1,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b₁ . 7 = <*(<*0,1,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b₁ . 8 = <*(<*1,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b₁ . 9 = <*(<*0,0,0,1*> ^ <*1,0,1,1*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & b₁ . 10 = <*(<*0,0,1,1*> ^ <*0,1,1,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> ) by R1, R2, R3, R4, R5, R10, R20, R30, R40, R50; :: thesis: verum