let n be non empty Element of NAT ; :: thesis: for m, k1, k2 being FinSequence of NAT st (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 & k2 . 1 = INV_MOD (k1 . 1),n & k2 . 2 = NEG_MOD (k1 . 3),n & k2 . 3 = NEG_MOD (k1 . 2),n & k2 . 4 = INV_MOD (k1 . 4),n holds
IDEAoperationA (IDEAoperationC (IDEAoperationA (IDEAoperationC m),k1,n)),k2,n = m
let m, k1, k2 be FinSequence of NAT ; :: thesis: ( (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 & k2 . 1 = INV_MOD (k1 . 1),n & k2 . 2 = NEG_MOD (k1 . 3),n & k2 . 3 = NEG_MOD (k1 . 2),n & k2 . 4 = INV_MOD (k1 . 4),n implies IDEAoperationA (IDEAoperationC (IDEAoperationA (IDEAoperationC m),k1,n)),k2,n = m )
assume that
A1: (2 to_power n) + 1 is prime and
A2: len m >= 4 and
A3: m . 1 is_expressible_by n and
A4: m . 2 is_expressible_by n and
A5: m . 3 is_expressible_by n and
A6: m . 4 is_expressible_by n and
A7: k1 . 1 is_expressible_by n and
A8: k1 . 2 is_expressible_by n and
A9: k1 . 3 is_expressible_by n and
A10: k1 . 4 is_expressible_by n and
A11: k2 . 1 = INV_MOD (k1 . 1),n and
A12: k2 . 2 = NEG_MOD (k1 . 3),n and
A13: k2 . 3 = NEG_MOD (k1 . 2),n and
A14: k2 . 4 = INV_MOD (k1 . 4),n ; :: thesis: IDEAoperationA (IDEAoperationC (IDEAoperationA (IDEAoperationC m),k1,n)),k2,n = m
A15: k2 . 1 is_expressible_by n by A1, A7, A11, Def10;
1 <= len m by A2, XXREAL_0:2;
then A16: 1 in Seg (len m) by FINSEQ_1:3;
then A17: 1 in dom m by FINSEQ_1:def 3;
A18: 4 in Seg (len m) by A2, FINSEQ_1:3;
then A19: 4 in dom m by FINSEQ_1:def 3;
3 <= len m by A2, XXREAL_0:2;
then A20: 3 in Seg (len m) by FINSEQ_1:3;
then A21: 3 in dom m by FINSEQ_1:def 3;
A22: k2 . 4 is_expressible_by n by A1, A10, A14, Def10;
consider I1 being FinSequence of NAT such that
A23: I1 = IDEAoperationC m ;
4 in Seg (len I1) by A23, A18, Def13;
then A24: 4 in dom I1 by FINSEQ_1:def 3;
1 in Seg (len I1) by A23, A16, Def13;
then A25: 1 in dom I1 by FINSEQ_1:def 3;
2 <= len m by A2, XXREAL_0:2;
then A26: 2 in Seg (len m) by FINSEQ_1:3;
then A27: 2 in dom m by FINSEQ_1:def 3;
3 in Seg (len I1) by A23, A20, Def13;
then A28: 3 in dom I1 by FINSEQ_1:def 3;
2 in Seg (len I1) by A23, A26, Def13;
then A29: 2 in dom I1 by FINSEQ_1:def 3;
consider I2 being FinSequence of NAT such that
A30: I2 = IDEAoperationA I1,k1,n ;
A31: len I2 = len I1 by A30, Def11;
then 2 in Seg (len I2) by A23, A26, Def13;
then A32: 2 in dom I2 by FINSEQ_1:def 3;
4 in Seg (len I2) by A23, A31, A18, Def13;
then A33: 4 in dom I2 by FINSEQ_1:def 3;
1 in Seg (len I2) by A23, A31, A16, Def13;
then A34: 1 in dom I2 by FINSEQ_1:def 3;
3 in Seg (len I2) by A23, A31, A20, Def13;
then A35: 3 in dom I2 by FINSEQ_1:def 3;
consider I3 being FinSequence of NAT such that
A36: I3 = IDEAoperationC I2 ;
A37: len I3 = len I2 by A36, Def13;
then 2 in Seg (len I3) by A23, A31, A26, Def13;
then A38: 2 in dom I3 by FINSEQ_1:def 3;
4 in Seg (len I3) by A23, A31, A37, A18, Def13;
then A39: 4 in dom I3 by FINSEQ_1:def 3;
3 in Seg (len I3) by A23, A31, A37, A20, Def13;
then A40: 3 in dom I3 by FINSEQ_1:def 3;
consider I4 being FinSequence of NAT such that
A41: I4 = IDEAoperationA I3,k2,n ;
1 in Seg (len I3) by A23, A31, A37, A16, Def13;
then A42: 1 in dom I3 by FINSEQ_1:def 3;

A43: now

let j be Nat; :: thesis: ( j in Seg (len m) implies I4 . j = m . j )
assume A44: j in Seg (len m) ; :: thesis: I4 . j = m . j
then A45: j in dom m by FINSEQ_1:def 3;
A46: j in Seg (len I1) by A23, A44, Def13;
then A47: j in Seg (len I2) by A30, Def11;
then A48: j in dom I2 by FINSEQ_1:def 3;
j in Seg (len I3) by A36, A47, Def13;
then A49: j in dom I3 by FINSEQ_1:def 3;
A50: j in dom I1 by A46, FINSEQ_1:def 3;

now

per cases ( j = 1 or j = 2 or j = 3 or j = 4 or ( j <> 1 & j <> 2 & j <> 3 & j <> 4 ) ) ;

suppose A51: j = 1 ; :: thesis: I4 . j = m . j

hence I4 . j = MUL_MOD (I3 . 1),(k2 . 1),n by A41, A42, Def11
.= MUL_MOD (I2 . 1),(k2 . 1),n by A36, A34, Lm5
.= MUL_MOD (MUL_MOD (I1 . 1),(k1 . 1),n),(k2 . 1),n by A30, A25, Def11
.= MUL_MOD (MUL_MOD (m . 1),(k1 . 1),n),(k2 . 1),n by A23, A17, Lm5
.= MUL_MOD (m . 1),(MUL_MOD (k1 . 1),(k2 . 1),n),n by A1, A3, A7, A15, Th24
.= MUL_MOD 1,(m . 1),n by A1, A7, A11, Def10
.= m . j by A3, A51, Th23 ;
:: thesis: verum

end;

suppose A52: j = 2 ; :: thesis: I4 . j = m . j

hence I4 . j = ADD_MOD (I3 . 2),(k2 . 2),n by A41, A38, Def11
.= ADD_MOD (I2 . 3),(k2 . 2),n by A36, A32, Lm3
.= ADD_MOD (ADD_MOD (I1 . 3),(k1 . 3),n),(k2 . 2),n by A30, A28, Def11
.= ADD_MOD (ADD_MOD (m . 2),(k1 . 3),n),(k2 . 2),n by A23, A21, Lm4
.= ADD_MOD (m . 2),(ADD_MOD (k1 . 3),(k2 . 2),n),n by Th15
.= ADD_MOD 0 ,(m . 2),n by A9, A12, Th12
.= m . j by A4, A52, Th14 ;
:: thesis: verum

end;

suppose A53: j = 3 ; :: thesis: I4 . j = m . j

hence I4 . j = ADD_MOD (I3 . 3),(k2 . 3),n by A41, A40, Def11
.= ADD_MOD (I2 . 2),(k2 . 3),n by A36, A35, Lm4
.= ADD_MOD (ADD_MOD (I1 . 2),(k1 . 2),n),(k2 . 3),n by A30, A29, Def11
.= ADD_MOD (ADD_MOD (m . 3),(k1 . 2),n),(k2 . 3),n by A23, A27, Lm3
.= ADD_MOD (m . 3),(ADD_MOD (k1 . 2),(k2 . 3),n),n by Th15
.= ADD_MOD 0 ,(m . 3),n by A8, A13, Th12
.= m . j by A5, A53, Th14 ;
:: thesis: verum

end;

suppose A54: j = 4 ; :: thesis: I4 . j = m . j

hence I4 . j = MUL_MOD (I3 . 4),(k2 . 4),n by A41, A39, Def11
.= MUL_MOD (I2 . 4),(k2 . 4),n by A36, A33, Lm5
.= MUL_MOD (MUL_MOD (I1 . 4),(k1 . 4),n),(k2 . 4),n by A30, A24, Def11
.= MUL_MOD (MUL_MOD (m . 4),(k1 . 4),n),(k2 . 4),n by A23, A19, Lm5
.= MUL_MOD (m . 4),(MUL_MOD (k1 . 4),(k2 . 4),n),n by A1, A6, A10, A22, Th24
.= MUL_MOD 1,(m . 4),n by A1, A10, A14, Def10
.= m . j by A6, A54, Th23 ;
:: thesis: verum

end;

suppose A55: ( j <> 1 & j <> 2 & j <> 3 & j <> 4 ) ; :: thesis: I4 . j = m . j

hence I4 . j = I3 . j by A41, A49, Def11
.= I2 . j by A36, A48, A55, Lm5
.= I1 . j by A30, A50, A55, Def11
.= m . j by A23, A45, A55, Lm5 ;
:: thesis: verum

end;

end;

end;

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

end;

A56: Seg (len m) = dom m by FINSEQ_1:def 3;
Seg (len m) = Seg (len I1) by A23, Def13
.= Seg (len I2) by A30, Def11
.= Seg (len I3) by A36, Def13
.= Seg (len I4) by A41, Def11
.= dom I4 by FINSEQ_1:def 3 ;
hence IDEAoperationA (IDEAoperationC (IDEAoperationA (IDEAoperationC m),k1,n)),k2,n = m by A23, A30, A36, A41, A56, A43, FINSEQ_1:17; :: thesis: verum