for SBT being Permutation of (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) . ((ShiftRows * (SubBytes SBT)) . text) = text