theorem :: AESCIP_1:26

( ShiftRows is one-to-one & ShiftRows is onto & InvShiftRows is one-to-one & InvShiftRows is onto & InvShiftRows = ShiftRows " & ShiftRows = InvShiftRows " ) by INV00, INV04, INV05;