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 . 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 & 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 . 2),n and
A4: k2 . 3 = NEG_MOD (k1 . 3),n and
A5: k2 . 4 = INV_MOD (k1 . 4),n ; :: thesis: IDEAoperationA (IDEAoperationA m,k1,n),k2,n = m
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 = IDEAoperationA m,k1,n ;
consider I2 being FinSequence of NAT such that
A9: I2 = IDEAoperationA I1,k2,n ;
A10: Seg (len m) = dom m by FINSEQ_1:def 3;
A11: Seg (len m) = Seg (len I1) by A8, Def11
.= Seg (len I2) by A9, Def11
.= dom I2 by FINSEQ_1:def 3 ;
Seg (len m) = dom m by FINSEQ_1:def 3;
then A12: 4 in dom m by A1, FINSEQ_1:3;
3 <= len m by A1, XXREAL_0:2;
then 3 in Seg (len m) by FINSEQ_1:3;
then A13: 3 in dom m by FINSEQ_1:def 3;
2 <= len m by A1, XXREAL_0:2;
then 2 in Seg (len m) by FINSEQ_1:3;
then A14: 2 in dom m by FINSEQ_1:def 3;
1 <= len m by A1, XXREAL_0:2;
then 1 in Seg (len m) by FINSEQ_1:3;
then A15: 1 in dom m by FINSEQ_1:def 3;

now

let j be Nat; :: thesis: ( j in Seg (len m) implies I2 . j = m . j )
assume A16: j in Seg (len m) ; :: thesis: I2 . j = m . j
then j in Seg (len I1) by A8, Def11;
then A17: j in dom I1 by FINSEQ_1:def 3;
A18: j in dom m by A16, 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 A19: j = 1 ; :: thesis: I2 . j = m . j

hence I2 . j = MUL_MOD (I1 . 1),(k2 . 1),n by A9, A17, Def11
.= MUL_MOD (MUL_MOD (m . 1),(k1 . 1),n),(k2 . 1),n by A8, A15, Def11
.= 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, A19, Th23 ;
:: thesis: verum

end;

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

hence I2 . j = ADD_MOD (I1 . 2),(k2 . 2),n by A9, A17, Def11
.= ADD_MOD (ADD_MOD (m . 2),(k1 . 2),n),(k2 . 2),n by A8, A14, Def11
.= ADD_MOD (m . 2),(ADD_MOD (k1 . 2),(k2 . 2),n),n by Th15
.= ADD_MOD 0 ,(m . 2),n by A1, A3, Th12
.= m . j by A1, A20, Th14 ;
:: thesis: verum

end;

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

hence I2 . j = ADD_MOD (I1 . 3),(k2 . 3),n by A9, A17, Def11
.= ADD_MOD (ADD_MOD (m . 3),(k1 . 3),n),(k2 . 3),n by A8, A13, Def11
.= ADD_MOD (m . 3),(ADD_MOD (k1 . 3),(k2 . 3),n),n by Th15
.= ADD_MOD 0 ,(m . 3),n by A1, A4, Th12
.= m . j by A1, A21, Th14 ;
:: thesis: verum

end;

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

hence I2 . j = MUL_MOD (I1 . 4),(k2 . 4),n by A9, A17, Def11
.= MUL_MOD (MUL_MOD (m . 4),(k1 . 4),n),(k2 . 4),n by A8, A12, Def11
.= 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, A22, Th23 ;
:: thesis: verum

end;

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

hence I2 . j = I1 . j by A9, A17, Def11
.= m . j by A8, A18, A23, Def11 ;
:: thesis: verum

end;

end;

end;

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

end;

hence IDEAoperationA (IDEAoperationA m,k1,n),k2,n = m by A8, A9, A10, A11, FINSEQ_1:17; :: thesis: verum