for cipher being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds AES-Statearray . ((AES-Statearray ") . cipher) = cipher