for x1, x2 being object st x1 in 128 -tuples_on BOOLEAN & x2 in 128 -tuples_on BOOLEAN & AES-Statearray . x1 = AES-Statearray . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in 128 -tuples_on BOOLEAN & x2 in 128 -tuples_on BOOLEAN & AES-Statearray . x1 = AES-Statearray . x2 implies x1 = x2 )
assume A1: ( x1 in 128 -tuples_on BOOLEAN & x2 in 128 -tuples_on BOOLEAN & AES-Statearray . x1 = AES-Statearray . x2 ) ; :: thesis: x1 = x2
then reconsider xx1 = x1, xx2 = x2 as Element of 128 -tuples_on BOOLEAN ;
P1: ex s being Element of BOOLEAN * st
( xx1 = s & len s = 128 ) by A1;
P2: ex s being Element of BOOLEAN * st
( xx2 = s & len s = 128 ) by A1;

now :: thesis: for k being Nat st 1 <= k & k <= len xx1 holds
xx1 . k = xx2 . k

let k be Nat; :: thesis: ( 1 <= k & k <= len xx1 implies xx1 . k = xx2 . k )
assume P5: ( 1 <= k & k <= len xx1 ) ; :: thesis: xx1 . k = xx2 . k
consider i, j being Nat such that
A4: ( i in Seg 4 & j in Seg 4 & (1 + ((i -' 1) * 8)) + ((j -' 1) * 32) <= k & k <= ((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7 ) by LMStat0, P5, P1;
mid (xx1,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7)) is Element of BOOLEAN * by FINSEQ_1:def 11;
then reconsider A1ij = ((AES-Statearray . xx1) . i) . j as FinSequence of BOOLEAN by DefStatearray, A4;
mid (xx2,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7)) is Element of BOOLEAN * by FINSEQ_1:def 11;
then reconsider A2ij = ((AES-Statearray . xx2) . i) . j as FinSequence of BOOLEAN by DefStatearray, A4;
A50: ((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) - (((i -' 1) * 8) + ((j -' 1) * 32)) <= k - (((i -' 1) * 8) + ((j -' 1) * 32)) by A4, XREAL_1:9;
then reconsider n = k - (((i -' 1) * 8) + ((j -' 1) * 32)) as Element of NAT by INT_1:3;
F41: k - (((i -' 1) * 8) + ((j -' 1) * 32)) <= (((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7) - (((i -' 1) * 8) + ((j -' 1) * 32)) by A4, XREAL_1:9;
F1: 1 <= 1 + (((i -' 1) * 8) + ((j -' 1) * 32)) by NAT_1:11;
F2: (1 + ((i -' 1) * 8)) + ((j -' 1) * 32) <= ((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7 by NAT_1:11;
Q110: ( 1 <= i & i <= 4 ) by A4, FINSEQ_1:1;
then 1 - 1 <= i - 1 by XREAL_1:9;
then i -' 1 = i - 1 by XREAL_0:def 2;
then i -' 1 <= 4 - 1 by Q110, XREAL_1:9;
then Q112: (i -' 1) * 8 <= 3 * 8 by XREAL_1:64;
Q130: ( 1 <= j & j <= 4 ) by A4, FINSEQ_1:1;
then 1 - 1 <= j - 1 by XREAL_1:9;
then j -' 1 = j - 1 by XREAL_0:def 2;
then j -' 1 <= 4 - 1 by Q130, XREAL_1:9;
then Q133: (j -' 1) * 32 <= 3 * 32 by XREAL_1:64;
((i -' 1) * 8) + ((j -' 1) * 32) <= 24 + 96 by Q133, Q112, XREAL_1:7;
then 1 + (((i -' 1) * 8) + ((j -' 1) * 32)) <= 1 + 120 by XREAL_1:7;
then Q135: ((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7 <= 121 + 7 by XREAL_1:6;
F5: n <= ((((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7) - ((1 + ((i -' 1) * 8)) + ((j -' 1) * 32))) + 1 by F41;
A6: k = (n - 1) + ((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) ;
thus xx1 . k = (mid (xx1,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7))) . n by F1, F2, Q135, P1, A50, F5, A6, FINSEQ_6:122
.= A2ij . n by DefStatearray, A4, A1
.= (mid (xx2,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7))) . n by DefStatearray, A4
.= xx2 . k by F1, F2, P2, Q135, A50, F5, A6, FINSEQ_6:122 ; :: thesis: verum

end;

hence x1 = x2 by P1, P2, FINSEQ_1:def 18; :: thesis: verum

end;

hence AES-Statearray is one-to-one by FUNCT_2:19; :: thesis: verum