let SBT be Permutation of (8 -tuples_on BOOLEAN); :: thesis: for output being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds (SubBytes SBT) . ((InvSubBytes SBT) . output) = output
let input be Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)); :: thesis: (SubBytes SBT) . ((InvSubBytes SBT) . input) = input

now :: thesis: for i, j being Nat st i in Seg 4 & j in Seg 4 holds
(((SubBytes SBT) . ((InvSubBytes SBT) . input)) . i) . j = (input . i) . j

let i, j be Nat; :: thesis: ( i in Seg 4 & j in Seg 4 implies (((SubBytes SBT) . ((InvSubBytes SBT) . input)) . i) . j = (input . i) . j )
assume A3: ( i in Seg 4 & j in Seg 4 ) ; :: thesis: (((SubBytes SBT) . ((InvSubBytes SBT) . input)) . i) . j = (input . i) . j
then consider outputij being Element of 8 -tuples_on BOOLEAN such that
A4: ( outputij = (((InvSubBytes SBT) . input) . i) . j & (((SubBytes SBT) . ((InvSubBytes SBT) . input)) . i) . j = SBT . outputij ) by DefSubBytes;
consider inputij being Element of 8 -tuples_on BOOLEAN such that
A5: ( inputij = (input . i) . j & (((InvSubBytes SBT) . input) . i) . j = (SBT ") . inputij ) by DefInvSubBytes, A3;
thus (((SubBytes SBT) . ((InvSubBytes SBT) . input)) . i) . j = (input . i) . j by A4, A5, INV08A; :: thesis: verum

end;

hence (SubBytes SBT) . ((InvSubBytes SBT) . input) = input by LM01; :: thesis: verum