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