let SBT be Permutation of (8 -tuples_on BOOLEAN); :: thesis: for m, i being Nat
for text being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for Key being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for eKeyi, dKeyi being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st ( m = 4 or m = 6 or m = 8 ) & i <= (7 + m) - 1 & eKeyi = ((KeyExpansion (SBT,m)) . Key) . ((7 + m) - i) & dKeyi = (Rev ((KeyExpansion (SBT,m)) . Key)) . (i + 1) holds
AddRoundKey . ((AddRoundKey . (text,eKeyi)),dKeyi) = text
let m, i be Nat; :: thesis: for text being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for Key being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for eKeyi, dKeyi being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st ( m = 4 or m = 6 or m = 8 ) & i <= (7 + m) - 1 & eKeyi = ((KeyExpansion (SBT,m)) . Key) . ((7 + m) - i) & dKeyi = (Rev ((KeyExpansion (SBT,m)) . Key)) . (i + 1) holds
AddRoundKey . ((AddRoundKey . (text,eKeyi)),dKeyi) = text
let text be Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)); :: thesis: for Key being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for eKeyi, dKeyi being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st ( m = 4 or m = 6 or m = 8 ) & i <= (7 + m) - 1 & eKeyi = ((KeyExpansion (SBT,m)) . Key) . ((7 + m) - i) & dKeyi = (Rev ((KeyExpansion (SBT,m)) . Key)) . (i + 1) holds
AddRoundKey . ((AddRoundKey . (text,eKeyi)),dKeyi) = text
let key be Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)); :: thesis: for eKeyi, dKeyi being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st ( m = 4 or m = 6 or m = 8 ) & i <= (7 + m) - 1 & eKeyi = ((KeyExpansion (SBT,m)) . key) . ((7 + m) - i) & dKeyi = (Rev ((KeyExpansion (SBT,m)) . key)) . (i + 1) holds
AddRoundKey . ((AddRoundKey . (text,eKeyi)),dKeyi) = text
let ekeyi, dkeyi be Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)); :: thesis: ( ( m = 4 or m = 6 or m = 8 ) & i <= (7 + m) - 1 & ekeyi = ((KeyExpansion (SBT,m)) . key) . ((7 + m) - i) & dkeyi = (Rev ((KeyExpansion (SBT,m)) . key)) . (i + 1) implies AddRoundKey . ((AddRoundKey . (text,ekeyi)),dkeyi) = text )
assume AS: ( ( m = 4 or m = 6 or m = 8 ) & i <= (7 + m) - 1 & ekeyi = ((KeyExpansion (SBT,m)) . key) . ((7 + m) - i) & dkeyi = (Rev ((KeyExpansion (SBT,m)) . key)) . (i + 1) ) ; :: thesis: AddRoundKey . ((AddRoundKey . (text,ekeyi)),dkeyi) = text
set p = (KeyExpansion (SBT,m)) . key;
(KeyExpansion (SBT,m)) . key in (7 + m) -tuples_on (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) ;
then B0: ex s being Element of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) * st
( (KeyExpansion (SBT,m)) . key = s & len s = 7 + m ) ;
i + 1 <= ((7 + m) - 1) + 1 by AS, XREAL_1:7;
then ( 1 <= i + 1 & i + 1 <= 7 + m ) by NAT_1:11;
then i + 1 in Seg (7 + m) ;
then B1: i + 1 in dom ((KeyExpansion (SBT,m)) . key) by FINSEQ_1:def 3, B0;
A0: dkeyi = ((KeyExpansion (SBT,m)) . key) . (((len ((KeyExpansion (SBT,m)) . key)) - (i + 1)) + 1) by AS, FINSEQ_5:58, B1
.= ekeyi by B0, AS ;

now :: thesis: for i, j being Nat st i in Seg 4 & j in Seg 4 holds
((AddRoundKey . ((AddRoundKey . (text,ekeyi)),dkeyi)) . i) . j = (text . i) . j

let i, j be Nat; :: thesis: ( i in Seg 4 & j in Seg 4 implies ((AddRoundKey . ((AddRoundKey . (text,ekeyi)),dkeyi)) . i) . j = (text . i) . j )
assume A3: ( i in Seg 4 & j in Seg 4 ) ; :: thesis: ((AddRoundKey . ((AddRoundKey . (text,ekeyi)),dkeyi)) . i) . j = (text . i) . j
then consider etextij, ekeyij being Element of 8 -tuples_on BOOLEAN such that
A4: ( etextij = (text . i) . j & ekeyij = (ekeyi . i) . j & ((AddRoundKey . (text,ekeyi)) . i) . j = Op-XOR (etextij,ekeyij) ) by DefAddRoundKey;
consider dtextij, dkeyij being Element of 8 -tuples_on BOOLEAN such that
A5: ( dtextij = ((AddRoundKey . (text,ekeyi)) . i) . j & dkeyij = (dkeyi . i) . j & ((AddRoundKey . ((AddRoundKey . (text,ekeyi)),dkeyi)) . i) . j = Op-XOR (dtextij,dkeyij) ) by DefAddRoundKey, A3;
thus ((AddRoundKey . ((AddRoundKey . (text,ekeyi)),dkeyi)) . i) . j = (text . i) . j by A4, A5, A0, DESCIP_1:17; :: thesis: verum

end;

hence AddRoundKey . ((AddRoundKey . (text,ekeyi)),dkeyi) = text by LM01; :: thesis: verum