theorem INV04: :: AESCIP_1:24

for input being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds InvShiftRows . (ShiftRows . input) = input