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

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

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

end;

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