theorem INV01: :: AESCIP_1:27

for MCFunc being Permutation of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)))
for input being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds (MCFunc ") . (MCFunc . input) = input