rng AES-Statearray = 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) by FUNCT_2:def 3;
then AES-Statearray " is Function of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))),(128 -tuples_on BOOLEAN) by FUNCT_2:25;
hence (AES-Statearray ") . (AES-DEC (SBT,MixColumns,(AES-Statearray . cipher),(AES-KeyInitState128 Key))) is Element of 128 -tuples_on BOOLEAN by FUNCT_2:5; :: thesis: verum