let cipher be Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)); :: thesis: AES-Statearray . ((AES-Statearray ") . cipher) = cipher
set f = AES-Statearray ;
L0: rng AES-Statearray = 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) by FUNCT_2:def 3;
then reconsider g = AES-Statearray " as Function of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))),(128 -tuples_on BOOLEAN) by FUNCT_2:25;
L2: ( (AES-Statearray ") * AES-Statearray = id (128 -tuples_on BOOLEAN) & AES-Statearray * (AES-Statearray ") = id (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) ) by FUNCT_2:29, L0;
then ( g is one-to-one & rng g = 128 -tuples_on BOOLEAN ) by FUNCT_2:18;
then AES-Statearray = g " by FUNCT_2:30, L2;
hence AES-Statearray . ((AES-Statearray ") . cipher) = cipher by FUNCT_2:26; :: thesis: verum