let n be non zero 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 . 2),n) & k2 . 3 = NEG_MOD ((k1 . 3),n) & k2 . 4 = INV_MOD ((k1 . 4),n) holds
IDEAoperationA ((IDEAoperationA (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 . 2),n) & k2 . 3 = NEG_MOD ((k1 . 3),n) & k2 . 4 = INV_MOD ((k1 . 4),n) implies IDEAoperationA ((IDEAoperationA (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 . 2),n) and
A13: k2 . 3 = NEG_MOD ((k1 . 3),n) and
A14: k2 . 4 = INV_MOD ((k1 . 4),n) ; :: thesis: IDEAoperationA ((IDEAoperationA (m,k1,n)),k2,n) = m
A15: k2 . 4 is_expressible_by n by A1, A10, A14, Def10;
2 <= len m by A2, XXREAL_0:2;
then 2 in Seg (len m) by FINSEQ_1:1;
then A16: 2 in dom m by FINSEQ_1:def 3;
Seg (len m) = dom m by FINSEQ_1:def 3;
then A17: 4 in dom m by A2, FINSEQ_1:1;
1 <= len m by A2, XXREAL_0:2;
then 1 in Seg (len m) by FINSEQ_1:1;
then A18: 1 in dom m by FINSEQ_1:def 3;
3 <= len m by A2, XXREAL_0:2;
then 3 in Seg (len m) by FINSEQ_1:1;
then A19: 3 in dom m by FINSEQ_1:def 3;
consider I1 being FinSequence of NAT such that
A20: I1 = IDEAoperationA (m,k1,n) ;
consider I2 being FinSequence of NAT such that
A21: I2 = IDEAoperationA (I1,k2,n) ;
A22: k2 . 1 is_expressible_by n by A1, A7, A11, Def10;

A23: now :: thesis: for j being Nat st j in Seg (len m) holds
I2 . j = m . j

let j be Nat; :: thesis: ( j in Seg (len m) implies I2 . j = m . j )
assume A24: j in Seg (len m) ; :: thesis: I2 . j = m . j
then j in Seg (len I1) by A20, Def11;
then A25: j in dom I1 by FINSEQ_1:def 3;
A26: j in dom m by A24, FINSEQ_1:def 3;

now :: thesis: I2 . j = m . j

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

suppose A27: j = 1 ; :: thesis: I2 . j = m . j

hence I2 . j = MUL_MOD ((I1 . 1),(k2 . 1),n) by A21, A25, Def11
.= MUL_MOD ((MUL_MOD ((m . 1),(k1 . 1),n)),(k2 . 1),n) by A20, A18, Def11
.= MUL_MOD ((m . 1),(MUL_MOD ((k1 . 1),(k2 . 1),n)),n) by A1, A3, A7, A22, Th23
.= MUL_MOD (1,(m . 1),n) by A1, A7, A11, Def10
.= m . j by A3, A27, Th22 ;
:: thesis: verum

end;

suppose A28: j = 2 ; :: thesis: I2 . j = m . j

hence I2 . j = ADD_MOD ((I1 . 2),(k2 . 2),n) by A21, A25, Def11
.= ADD_MOD ((ADD_MOD ((m . 2),(k1 . 2),n)),(k2 . 2),n) by A20, A16, Def11
.= ADD_MOD ((m . 2),(ADD_MOD ((k1 . 2),(k2 . 2),n)),n) by Th14
.= ADD_MOD (0,(m . 2),n) by A8, A12, Th11
.= m . j by A4, A28, Th13 ;
:: thesis: verum

end;

suppose A29: j = 3 ; :: thesis: I2 . j = m . j

hence I2 . j = ADD_MOD ((I1 . 3),(k2 . 3),n) by A21, A25, Def11
.= ADD_MOD ((ADD_MOD ((m . 3),(k1 . 3),n)),(k2 . 3),n) by A20, A19, Def11
.= ADD_MOD ((m . 3),(ADD_MOD ((k1 . 3),(k2 . 3),n)),n) by Th14
.= ADD_MOD (0,(m . 3),n) by A9, A13, Th11
.= m . j by A5, A29, Th13 ;
:: thesis: verum

end;

suppose A30: j = 4 ; :: thesis: I2 . j = m . j

hence I2 . j = MUL_MOD ((I1 . 4),(k2 . 4),n) by A21, A25, Def11
.= MUL_MOD ((MUL_MOD ((m . 4),(k1 . 4),n)),(k2 . 4),n) by A20, A17, Def11
.= MUL_MOD ((m . 4),(MUL_MOD ((k1 . 4),(k2 . 4),n)),n) by A1, A6, A10, A15, Th23
.= MUL_MOD (1,(m . 4),n) by A1, A10, A14, Def10
.= m . j by A6, A30, Th22 ;
:: thesis: verum

end;

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

hence I2 . j = I1 . j by A21, A25, Def11
.= m . j by A20, A26, A31, Def11 ;
:: thesis: verum

end;

end;

end;

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

end;

A32: Seg (len m) = dom m by FINSEQ_1:def 3;
Seg (len m) = Seg (len I1) by A20, Def11
.= Seg (len I2) by A21, Def11
.= dom I2 by FINSEQ_1:def 3 ;
hence IDEAoperationA ((IDEAoperationA (m,k1,n)),k2,n) = m by A20, A21, A32, A23, FINSEQ_1:13; :: thesis: verum