let D be non empty set ; :: thesis: for n being non zero Element of NAT
for r being Element of n -tuples_on D st 8 <= n & 8 <= n - 8 & 16 <= n & 8 <= n - 16 & 24 <= n & 8 <= n - 24 holds
<*(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))*> is Element of 4 -tuples_on (8 -tuples_on D)
let n be non zero Element of NAT ; :: thesis: for r being Element of n -tuples_on D st 8 <= n & 8 <= n - 8 & 16 <= n & 8 <= n - 16 & 24 <= n & 8 <= n - 24 holds
<*(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))*> is Element of 4 -tuples_on (8 -tuples_on D)
let r be Element of n -tuples_on D; :: thesis: ( 8 <= n & 8 <= n - 8 & 16 <= n & 8 <= n - 16 & 24 <= n & 8 <= n - 24 implies <*(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))*> is Element of 4 -tuples_on (8 -tuples_on D) )
assume ( 8 <= n & 8 <= n - 8 & 16 <= n & 8 <= n - 16 & 24 <= n & 8 <= n - 24 ) ; :: thesis: <*(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))*> is Element of 4 -tuples_on (8 -tuples_on D)
then ( Op-Left (r,8) is Element of 8 -tuples_on D & Op-Left ((Op-Right (r,8)),8) is Element of 8 -tuples_on D & Op-Left ((Op-Right (r,16)),8) is Element of 8 -tuples_on D & Op-Left ((Op-Right (r,24)),8) is Element of 8 -tuples_on D ) by DESCIP_1:1, LR8D1;
hence <*(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))*> is Element of 4 -tuples_on (8 -tuples_on D) by LMGSEQ4; :: thesis: verum