theorem INV05: :: AESCIP_1:25

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