let SBT be Permutation of (8 -tuples_on BOOLEAN); :: thesis: for MCFunc being Permutation of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)))
for m being Nat
for text being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds (((InvSubBytes SBT) * InvShiftRows) * (MCFunc ")) . (((MCFunc * ShiftRows) * (SubBytes SBT)) . text) = text
let MCFunc be Permutation of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))); :: thesis: for m being Nat
for text being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds (((InvSubBytes SBT) * InvShiftRows) * (MCFunc ")) . (((MCFunc * ShiftRows) * (SubBytes SBT)) . text) = text
let m be Nat; :: thesis: for text being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds (((InvSubBytes SBT) * InvShiftRows) * (MCFunc ")) . (((MCFunc * ShiftRows) * (SubBytes SBT)) . text) = text
let text be Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)); :: thesis: (((InvSubBytes SBT) * InvShiftRows) * (MCFunc ")) . (((MCFunc * ShiftRows) * (SubBytes SBT)) . text) = text
thus (((InvSubBytes SBT) * InvShiftRows) * (MCFunc ")) . (((MCFunc * ShiftRows) * (SubBytes SBT)) . text) = (((InvSubBytes SBT) * InvShiftRows) * (MCFunc ")) . ((MCFunc * ShiftRows) . ((SubBytes SBT) . text)) by FUNCT_2:15
.= (((InvSubBytes SBT) * InvShiftRows) * (MCFunc ")) . (MCFunc . (ShiftRows . ((SubBytes SBT) . text))) by FUNCT_2:15
.= ((InvSubBytes SBT) * InvShiftRows) . ((MCFunc ") . (MCFunc . (ShiftRows . ((SubBytes SBT) . text)))) by FUNCT_2:15
.= ((InvSubBytes SBT) * InvShiftRows) . (ShiftRows . ((SubBytes SBT) . text)) by INV01
.= (InvSubBytes SBT) . (InvShiftRows . (ShiftRows . ((SubBytes SBT) . text))) by FUNCT_2:15
.= (InvSubBytes SBT) . ((SubBytes SBT) . text) by INV04
.= text by INV07 ; :: thesis: verum