let n be non empty Element of NAT ; :: thesis:
let m, k1, k2 be FinSequence of NAT ; :: thesis:
assume that
A1: ( (2 to_power n) + 1 is prime & len m >= 4 & m . 1 is_expressible_by n & m . 2 is_expressible_by n & m . 3 is_expressible_by n & m . 4 is_expressible_by n & k1 . 1 is_expressible_by n & k1 . 2 is_expressible_by n & k1 . 3 is_expressible_by n & k1 . 4 is_expressible_by n ) and
A2: k2 . 1 = INV_MOD (k1 . 1),n and
A3: k2 . 2 = NEG_MOD (k1 . 3),n and
A4: k2 . 3 = NEG_MOD (k1 . 2),n and
A5: k2 . 4 = INV_MOD (k1 . 4),n ; :: thesis:
A6: k2 . 1 is_expressible_by n by A1, A2, Def10;
A7: k2 . 4 is_expressible_by n by A1, A5, Def10;
consider I1 being FinSequence of NAT such that
A8: I1 = IDEAoperationC m ;
consider I2 being FinSequence of NAT such that
A9: I2 = IDEAoperationA I1,k1,n ;
A10: ( len I2 = len I1 & ( for i being Element of NAT st i in dom I1 holds
( ( i = 1 implies I2 . i = MUL_MOD (I1 . 1),(k1 . 1),n ) & ( i = 2 implies I2 . i = ADD_MOD (I1 . 2),(k1 . 2),n ) & ( i = 3 implies I2 . i = ADD_MOD (I1 . 3),(k1 . 3),n ) & ( i = 4 implies I2 . i = MUL_MOD (I1 . 4),(k1 . 4),n ) & ( i <> 1 & i <> 2 & i <> 3 & i <> 4 implies I2 . i = I1 . i ) ) ) ) by A9, Def11;
consider I3 being FinSequence of NAT such that
A11: I3 = IDEAoperationC I2 ;
A12: ( len I3 = len I2 & ( for i being Element of NAT st i in dom I2 holds
( ( i = 2 implies I3 . i = I2 . 3 ) & ( i = 3 implies I3 . i = I2 . 2 ) & ( i <> 2 & i <> 3 implies I3 . i = I2 . i ) ) ) ) by A11, Def13, Lm3, Lm4, Lm5;
consider I4 being FinSequence of NAT such that
A13: I4 = IDEAoperationA I3,k2,n ;
A14: ( len I4 = len I3 & ( for i being Element of NAT st i in dom I3 holds
( ( i = 1 implies I4 . i = MUL_MOD (I3 . 1),(k2 . 1),n ) & ( i = 2 implies I4 . i = ADD_MOD (I3 . 2),(k2 . 2),n ) & ( i = 3 implies I4 . i = ADD_MOD (I3 . 3),(k2 . 3),n ) & ( i = 4 implies I4 . i = MUL_MOD (I3 . 4),(k2 . 4),n ) & ( i <> 1 & i <> 2 & i <> 3 & i <> 4 implies I4 . i = I3 . i ) ) ) ) by A13, Def11;
A15: Seg (len m) = dom m by FINSEQ_1:def 3;
A16: Seg (len m) = Seg (len I1) by A8, Def13
.= Seg (len I2) by A9, Def11
.= Seg (len I3) by A11, Def13
.= Seg (len I4) by A13, Def11
.= dom I4 by FINSEQ_1:def 3 ;
1 <= len m by A1, XXREAL_0:2;
then A17: 1 in Seg (len m) by FINSEQ_1:3;
then ( 1 in Seg (len I1) & 1 in Seg (len I2) & 1 in Seg (len I3) & 1 in Seg (len I4) ) by A8, A10, A12, A14, Def13;
then A18: ( 1 in dom I1 & 1 in dom I2 & 1 in dom I3 & 1 in dom I4 ) by FINSEQ_1:def 3;
A19: 1 in dom m by A17, FINSEQ_1:def 3;
2 <= len m by A1, XXREAL_0:2;
then A20: 2 in Seg (len m) by FINSEQ_1:3;
then ( 2 in Seg (len I1) & 2 in Seg (len I2) & 2 in Seg (len I3) & 2 in Seg (len I4) ) by A8, A10, A12, A14, Def13;
then A21: ( 2 in dom I1 & 2 in dom I2 & 2 in dom I3 & 2 in dom I4 ) by FINSEQ_1:def 3;
A22: 2 in dom m by A20, FINSEQ_1:def 3;
3 <= len m by A1, XXREAL_0:2;
then A23: 3 in Seg (len m) by FINSEQ_1:3;
then ( 3 in Seg (len I1) & 3 in Seg (len I2) & 3 in Seg (len I3) & 3 in Seg (len I4) ) by A8, A10, A12, A14, Def13;
then A24: ( 3 in dom I1 & 3 in dom I2 & 3 in dom I3 & 3 in dom I4 ) by FINSEQ_1:def 3;
A25: 3 in dom m by A23, FINSEQ_1:def 3;
A26: 4 in Seg (len m) by A1, FINSEQ_1:3;
then ( 4 in Seg (len I1) & 4 in Seg (len I2) & 4 in Seg (len I3) & 4 in Seg (len I4) ) by A8, A10, A12, A14, Def13;
then A27: ( 4 in dom I1 & 4 in dom I2 & 4 in dom I3 & 4 in dom I4 ) by FINSEQ_1:def 3;
A28: 4 in dom m by A26, FINSEQ_1:def 3;

now

let j be Nat; :: thesis:
assume A29: j in Seg (len m) ; :: thesis:
then A30: j in Seg (len I1) by A8, Def13;
then A31: j in Seg (len I2) by A9, Def11;
then A32: j in Seg (len I3) by A11, Def13;
A33: j in dom I1 by A30, FINSEQ_1:def 3;
A34: j in dom I2 by A31, FINSEQ_1:def 3;
A35: j in dom I3 by A32, FINSEQ_1:def 3;
A36: j in dom m by A29, FINSEQ_1:def 3;

now

per cases ;

suppose A37: j = 1 ; :: thesis:

hence I4 . j = MUL_MOD (I3 . 1),(k2 . 1),n by A13, A18, Def11
.= MUL_MOD (I2 . 1),(k2 . 1),n by A11, A18, Lm5
.= MUL_MOD (MUL_MOD (I1 . 1),(k1 . 1),n),(k2 . 1),n by A9, A18, Def11
.= MUL_MOD (MUL_MOD (m . 1),(k1 . 1),n),(k2 . 1),n by A8, A19, Lm5
.= MUL_MOD (m . 1),(MUL_MOD (k1 . 1),(k2 . 1),n),n by A1, A6, Th24
.= MUL_MOD 1,(m . 1),n by A1, A2, Def10
.= m . j by A1, A37, Th23 ;
:: thesis:

end;

suppose A38: j = 2 ; :: thesis:

hence I4 . j = ADD_MOD (I3 . 2),(k2 . 2),n by A13, A21, Def11
.= ADD_MOD (I2 . 3),(k2 . 2),n by A11, A21, Lm3
.= ADD_MOD (ADD_MOD (I1 . 3),(k1 . 3),n),(k2 . 2),n by A9, A24, Def11
.= ADD_MOD (ADD_MOD (m . 2),(k1 . 3),n),(k2 . 2),n by A8, A25, Lm4
.= ADD_MOD (m . 2),(ADD_MOD (k1 . 3),(k2 . 2),n),n by Th15
.= ADD_MOD 0 ,(m . 2),n by A1, A3, Th12
.= m . j by A1, A38, Th14 ;
:: thesis:

end;

suppose A39: j = 3 ; :: thesis:

hence I4 . j = ADD_MOD (I3 . 3),(k2 . 3),n by A13, A24, Def11
.= ADD_MOD (I2 . 2),(k2 . 3),n by A11, A24, Lm4
.= ADD_MOD (ADD_MOD (I1 . 2),(k1 . 2),n),(k2 . 3),n by A9, A21, Def11
.= ADD_MOD (ADD_MOD (m . 3),(k1 . 2),n),(k2 . 3),n by A8, A22, Lm3
.= ADD_MOD (m . 3),(ADD_MOD (k1 . 2),(k2 . 3),n),n by Th15
.= ADD_MOD 0 ,(m . 3),n by A1, A4, Th12
.= m . j by A1, A39, Th14 ;
:: thesis:

end;

suppose A40: j = 4 ; :: thesis:

hence I4 . j = MUL_MOD (I3 . 4),(k2 . 4),n by A13, A27, Def11
.= MUL_MOD (I2 . 4),(k2 . 4),n by A11, A27, Lm5
.= MUL_MOD (MUL_MOD (I1 . 4),(k1 . 4),n),(k2 . 4),n by A9, A27, Def11
.= MUL_MOD (MUL_MOD (m . 4),(k1 . 4),n),(k2 . 4),n by A8, A28, Lm5
.= MUL_MOD (m . 4),(MUL_MOD (k1 . 4),(k2 . 4),n),n by A1, A7, Th24
.= MUL_MOD 1,(m . 4),n by A1, A5, Def10
.= m . j by A1, A40, Th23 ;
:: thesis:

end;

suppose A41: ( j <> 1 & j <> 2 & j <> 3 & j <> 4 ) ; :: thesis:

hence I4 . j = I3 . j by A13, A35, Def11
.= I2 . j by A11, A34, A41, Lm5
.= I1 . j by A9, A33, A41, Def11
.= m . j by A8, A36, A41, Lm5 ;
:: thesis:

end;

hence I4 . j = m . j ; :: thesis:

end;

hence IDEAoperationA (IDEAoperationC (IDEAoperationA (IDEAoperationC m),k1,n)),k2,n = m by A8, A9, A11, A13, A15, A16, FINSEQ_1:17; :: thesis: