theorem LAST02: :: AESCIP_1:30

for SBT being Permutation of (8 -tuples_on BOOLEAN)
for MCFunc being Permutation of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)))
for m being Nat
for text being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds (((InvSubBytes SBT) * InvShiftRows) * (MCFunc ")) . (((MCFunc * ShiftRows) * (SubBytes SBT)) . text) = text