:: deftheorem DefSubBytes defines SubBytes AESCIP_1:def 2 :
for SBT being Permutation of (8 -tuples_on BOOLEAN)
for b₂ being Function of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))),(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) holds
( b₂ = SubBytes SBT iff for input being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for i, j being Nat st i in Seg 4 & j in Seg 4 holds
ex inputij being Element of 8 -tuples_on BOOLEAN st
( inputij = (input . i) . j & ((b₂ . input) . i) . j = SBT . inputij ) );