theorem :: AESCIP_1:23

for SBT being Permutation of (8 -tuples_on BOOLEAN) holds
( SubBytes SBT is one-to-one & SubBytes SBT is onto & InvSubBytes SBT is one-to-one & InvSubBytes SBT is onto & InvSubBytes SBT = (SubBytes SBT) " & SubBytes SBT = (InvSubBytes SBT) " )