:: deftheorem defines SubWord AESCIP_1:def 7 :
for SBT being Permutation of (8 -tuples_on BOOLEAN)
for x, b₃ being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) holds
( b₃ = SubWord (SBT,x) iff for i being Element of Seg 4 holds b₃ . i = SBT . (x . i) );