theorem Th29: :: DESCIP_1:29

for r being Element of 48 -tuples_on BOOLEAN ex s1, s2, s3, s4, s5, s6, s7, s8 being Element of 6 -tuples_on BOOLEAN st
( s1 = (DES-DIV8 r) . 1 & s2 = (DES-DIV8 r) . 2 & s3 = (DES-DIV8 r) . 3 & s4 = (DES-DIV8 r) . 4 & s5 = (DES-DIV8 r) . 5 & s6 = (DES-DIV8 r) . 6 & s7 = (DES-DIV8 r) . 7 & s8 = (DES-DIV8 r) . 8 & r = ((((((s1 ^ s2) ^ s3) ^ s4) ^ s5) ^ s6) ^ s7) ^ s8 )