let D be non empty set ; for n, m, l, p, q being non zero Element of NAT
for r being Element of n -tuples_on D st m <= n & 8 <= n - m & l = m + 8 & l <= n & 8 <= n - l & p = m + 16 & p <= n & 8 <= n - p & q = m + 24 & q <= n & 8 = n - q holds
<*(Op-Left ((Op-Right (r,m)),8)),(Op-Left ((Op-Right (r,l)),8)),(Op-Left ((Op-Right (r,p)),8)),(Op-Right (r,q))*> is Element of 4 -tuples_on (8 -tuples_on D)
let n, m, l, p, q be non zero Element of NAT ; for r being Element of n -tuples_on D st m <= n & 8 <= n - m & l = m + 8 & l <= n & 8 <= n - l & p = m + 16 & p <= n & 8 <= n - p & q = m + 24 & q <= n & 8 = n - q holds
<*(Op-Left ((Op-Right (r,m)),8)),(Op-Left ((Op-Right (r,l)),8)),(Op-Left ((Op-Right (r,p)),8)),(Op-Right (r,q))*> is Element of 4 -tuples_on (8 -tuples_on D)
let r be Element of n -tuples_on D; ( m <= n & 8 <= n - m & l = m + 8 & l <= n & 8 <= n - l & p = m + 16 & p <= n & 8 <= n - p & q = m + 24 & q <= n & 8 = n - q implies <*(Op-Left ((Op-Right (r,m)),8)),(Op-Left ((Op-Right (r,l)),8)),(Op-Left ((Op-Right (r,p)),8)),(Op-Right (r,q))*> is Element of 4 -tuples_on (8 -tuples_on D) )
assume
( m <= n & 8 <= n - m & l = m + 8 & l <= n & 8 <= n - l & p = m + 16 & p <= n & 8 <= n - p & q = m + 24 & q <= n & 8 = n - q )
; <*(Op-Left ((Op-Right (r,m)),8)),(Op-Left ((Op-Right (r,l)),8)),(Op-Left ((Op-Right (r,p)),8)),(Op-Right (r,q))*> is Element of 4 -tuples_on (8 -tuples_on D)
then
( Op-Left ((Op-Right (r,m)),8) is Element of 8 -tuples_on D & Op-Left ((Op-Right (r,l)),8) is Element of 8 -tuples_on D & Op-Left ((Op-Right (r,p)),8) is Element of 8 -tuples_on D & Op-Right (r,q) is Element of 8 -tuples_on D )
by DESCIP_1:2, LR8D1;
hence
<*(Op-Left ((Op-Right (r,m)),8)),(Op-Left ((Op-Right (r,l)),8)),(Op-Left ((Op-Right (r,p)),8)),(Op-Right (r,q))*> is Element of 4 -tuples_on (8 -tuples_on D)
by LMGSEQ4; verum