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