let D be non empty set ; 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 ; 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; ( 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 )
; <*(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; verum