let SBT be Permutation of (8 -tuples_on BOOLEAN); :: thesis: ( 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) " )
set f = SubBytes SBT;
set g = InvSubBytes SBT;
P1: for x being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds (InvSubBytes SBT) . ((SubBytes SBT) . x) = x by INV07;
P2: for y being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds (SubBytes SBT) . ((InvSubBytes SBT) . y) = y by INV08;
thus ( 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) " ) by INV00, P1, P2; :: thesis: verum