let n be non zero Nat; for lk being Nat
for Key1, Key2 being Matrix of lk,6,NAT
for r being Nat
for ks1, ks2, ke1, ke2, m being FinSequence of NAT st lk >= r & (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 & ( for i being Nat st i <= r holds
( Key1 * (i,1) is_expressible_by n & Key1 * (i,2) is_expressible_by n & Key1 * (i,3) is_expressible_by n & Key1 * (i,4) is_expressible_by n & Key1 * (i,5) is_expressible_by n & Key1 * (i,6) is_expressible_by n & Key2 * (i,1) is_expressible_by n & Key2 * (i,2) is_expressible_by n & Key2 * (i,3) is_expressible_by n & Key2 * (i,4) is_expressible_by n & Key2 * (i,5) is_expressible_by n & Key2 * (i,6) is_expressible_by n & Key2 * (i,1) = INV_MOD ((Key1 * (i,1)),n) & Key2 * (i,2) = NEG_MOD ((Key1 * (i,3)),n) & Key2 * (i,3) = NEG_MOD ((Key1 * (i,2)),n) & Key2 * (i,4) = INV_MOD ((Key1 * (i,4)),n) & Key1 * (i,5) = Key2 * (i,5) & Key1 * (i,6) = Key2 * (i,6) ) ) & ks1 . 1 is_expressible_by n & ks1 . 2 is_expressible_by n & ks1 . 3 is_expressible_by n & ks1 . 4 is_expressible_by n & ks2 . 1 = INV_MOD ((ks1 . 1),n) & ks2 . 2 = NEG_MOD ((ks1 . 2),n) & ks2 . 3 = NEG_MOD ((ks1 . 3),n) & ks2 . 4 = INV_MOD ((ks1 . 4),n) & ke1 . 1 is_expressible_by n & ke1 . 2 is_expressible_by n & ke1 . 3 is_expressible_by n & ke1 . 4 is_expressible_by n & ke2 . 1 = INV_MOD ((ke1 . 1),n) & ke2 . 2 = NEG_MOD ((ke1 . 2),n) & ke2 . 3 = NEG_MOD ((ke1 . 3),n) & ke2 . 4 = INV_MOD ((ke1 . 4),n) & ke2 . 5 = ke1 . 5 & ke2 . 6 = ke1 . 6 holds
((IDEA_QS (ks2,n)) * ((compose ((IDEA_Q_F (Key2,n,r)),MESSAGES)) * ((IDEA_QE (ke2,n)) * ((IDEA_PE (ke1,n)) * ((compose ((IDEA_P_F (Key1,n,r)),MESSAGES)) * (IDEA_PS (ks1,n))))))) . m = m
let lk be Nat; for Key1, Key2 being Matrix of lk,6,NAT
for r being Nat
for ks1, ks2, ke1, ke2, m being FinSequence of NAT st lk >= r & (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 & ( for i being Nat st i <= r holds
( Key1 * (i,1) is_expressible_by n & Key1 * (i,2) is_expressible_by n & Key1 * (i,3) is_expressible_by n & Key1 * (i,4) is_expressible_by n & Key1 * (i,5) is_expressible_by n & Key1 * (i,6) is_expressible_by n & Key2 * (i,1) is_expressible_by n & Key2 * (i,2) is_expressible_by n & Key2 * (i,3) is_expressible_by n & Key2 * (i,4) is_expressible_by n & Key2 * (i,5) is_expressible_by n & Key2 * (i,6) is_expressible_by n & Key2 * (i,1) = INV_MOD ((Key1 * (i,1)),n) & Key2 * (i,2) = NEG_MOD ((Key1 * (i,3)),n) & Key2 * (i,3) = NEG_MOD ((Key1 * (i,2)),n) & Key2 * (i,4) = INV_MOD ((Key1 * (i,4)),n) & Key1 * (i,5) = Key2 * (i,5) & Key1 * (i,6) = Key2 * (i,6) ) ) & ks1 . 1 is_expressible_by n & ks1 . 2 is_expressible_by n & ks1 . 3 is_expressible_by n & ks1 . 4 is_expressible_by n & ks2 . 1 = INV_MOD ((ks1 . 1),n) & ks2 . 2 = NEG_MOD ((ks1 . 2),n) & ks2 . 3 = NEG_MOD ((ks1 . 3),n) & ks2 . 4 = INV_MOD ((ks1 . 4),n) & ke1 . 1 is_expressible_by n & ke1 . 2 is_expressible_by n & ke1 . 3 is_expressible_by n & ke1 . 4 is_expressible_by n & ke2 . 1 = INV_MOD ((ke1 . 1),n) & ke2 . 2 = NEG_MOD ((ke1 . 2),n) & ke2 . 3 = NEG_MOD ((ke1 . 3),n) & ke2 . 4 = INV_MOD ((ke1 . 4),n) & ke2 . 5 = ke1 . 5 & ke2 . 6 = ke1 . 6 holds
((IDEA_QS (ks2,n)) * ((compose ((IDEA_Q_F (Key2,n,r)),MESSAGES)) * ((IDEA_QE (ke2,n)) * ((IDEA_PE (ke1,n)) * ((compose ((IDEA_P_F (Key1,n,r)),MESSAGES)) * (IDEA_PS (ks1,n))))))) . m = m
let Key1, Key2 be Matrix of lk,6,NAT; for r being Nat
for ks1, ks2, ke1, ke2, m being FinSequence of NAT st lk >= r & (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 & ( for i being Nat st i <= r holds
( Key1 * (i,1) is_expressible_by n & Key1 * (i,2) is_expressible_by n & Key1 * (i,3) is_expressible_by n & Key1 * (i,4) is_expressible_by n & Key1 * (i,5) is_expressible_by n & Key1 * (i,6) is_expressible_by n & Key2 * (i,1) is_expressible_by n & Key2 * (i,2) is_expressible_by n & Key2 * (i,3) is_expressible_by n & Key2 * (i,4) is_expressible_by n & Key2 * (i,5) is_expressible_by n & Key2 * (i,6) is_expressible_by n & Key2 * (i,1) = INV_MOD ((Key1 * (i,1)),n) & Key2 * (i,2) = NEG_MOD ((Key1 * (i,3)),n) & Key2 * (i,3) = NEG_MOD ((Key1 * (i,2)),n) & Key2 * (i,4) = INV_MOD ((Key1 * (i,4)),n) & Key1 * (i,5) = Key2 * (i,5) & Key1 * (i,6) = Key2 * (i,6) ) ) & ks1 . 1 is_expressible_by n & ks1 . 2 is_expressible_by n & ks1 . 3 is_expressible_by n & ks1 . 4 is_expressible_by n & ks2 . 1 = INV_MOD ((ks1 . 1),n) & ks2 . 2 = NEG_MOD ((ks1 . 2),n) & ks2 . 3 = NEG_MOD ((ks1 . 3),n) & ks2 . 4 = INV_MOD ((ks1 . 4),n) & ke1 . 1 is_expressible_by n & ke1 . 2 is_expressible_by n & ke1 . 3 is_expressible_by n & ke1 . 4 is_expressible_by n & ke2 . 1 = INV_MOD ((ke1 . 1),n) & ke2 . 2 = NEG_MOD ((ke1 . 2),n) & ke2 . 3 = NEG_MOD ((ke1 . 3),n) & ke2 . 4 = INV_MOD ((ke1 . 4),n) & ke2 . 5 = ke1 . 5 & ke2 . 6 = ke1 . 6 holds
((IDEA_QS (ks2,n)) * ((compose ((IDEA_Q_F (Key2,n,r)),MESSAGES)) * ((IDEA_QE (ke2,n)) * ((IDEA_PE (ke1,n)) * ((compose ((IDEA_P_F (Key1,n,r)),MESSAGES)) * (IDEA_PS (ks1,n))))))) . m = m
let r be Nat; for ks1, ks2, ke1, ke2, m being FinSequence of NAT st lk >= r & (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 & ( for i being Nat st i <= r holds
( Key1 * (i,1) is_expressible_by n & Key1 * (i,2) is_expressible_by n & Key1 * (i,3) is_expressible_by n & Key1 * (i,4) is_expressible_by n & Key1 * (i,5) is_expressible_by n & Key1 * (i,6) is_expressible_by n & Key2 * (i,1) is_expressible_by n & Key2 * (i,2) is_expressible_by n & Key2 * (i,3) is_expressible_by n & Key2 * (i,4) is_expressible_by n & Key2 * (i,5) is_expressible_by n & Key2 * (i,6) is_expressible_by n & Key2 * (i,1) = INV_MOD ((Key1 * (i,1)),n) & Key2 * (i,2) = NEG_MOD ((Key1 * (i,3)),n) & Key2 * (i,3) = NEG_MOD ((Key1 * (i,2)),n) & Key2 * (i,4) = INV_MOD ((Key1 * (i,4)),n) & Key1 * (i,5) = Key2 * (i,5) & Key1 * (i,6) = Key2 * (i,6) ) ) & ks1 . 1 is_expressible_by n & ks1 . 2 is_expressible_by n & ks1 . 3 is_expressible_by n & ks1 . 4 is_expressible_by n & ks2 . 1 = INV_MOD ((ks1 . 1),n) & ks2 . 2 = NEG_MOD ((ks1 . 2),n) & ks2 . 3 = NEG_MOD ((ks1 . 3),n) & ks2 . 4 = INV_MOD ((ks1 . 4),n) & ke1 . 1 is_expressible_by n & ke1 . 2 is_expressible_by n & ke1 . 3 is_expressible_by n & ke1 . 4 is_expressible_by n & ke2 . 1 = INV_MOD ((ke1 . 1),n) & ke2 . 2 = NEG_MOD ((ke1 . 2),n) & ke2 . 3 = NEG_MOD ((ke1 . 3),n) & ke2 . 4 = INV_MOD ((ke1 . 4),n) & ke2 . 5 = ke1 . 5 & ke2 . 6 = ke1 . 6 holds
((IDEA_QS (ks2,n)) * ((compose ((IDEA_Q_F (Key2,n,r)),MESSAGES)) * ((IDEA_QE (ke2,n)) * ((IDEA_PE (ke1,n)) * ((compose ((IDEA_P_F (Key1,n,r)),MESSAGES)) * (IDEA_PS (ks1,n))))))) . m = m
let ks1, ks2, ke1, ke2 be FinSequence of NAT ; for m being FinSequence of NAT st lk >= r & (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 & ( for i being Nat st i <= r holds
( Key1 * (i,1) is_expressible_by n & Key1 * (i,2) is_expressible_by n & Key1 * (i,3) is_expressible_by n & Key1 * (i,4) is_expressible_by n & Key1 * (i,5) is_expressible_by n & Key1 * (i,6) is_expressible_by n & Key2 * (i,1) is_expressible_by n & Key2 * (i,2) is_expressible_by n & Key2 * (i,3) is_expressible_by n & Key2 * (i,4) is_expressible_by n & Key2 * (i,5) is_expressible_by n & Key2 * (i,6) is_expressible_by n & Key2 * (i,1) = INV_MOD ((Key1 * (i,1)),n) & Key2 * (i,2) = NEG_MOD ((Key1 * (i,3)),n) & Key2 * (i,3) = NEG_MOD ((Key1 * (i,2)),n) & Key2 * (i,4) = INV_MOD ((Key1 * (i,4)),n) & Key1 * (i,5) = Key2 * (i,5) & Key1 * (i,6) = Key2 * (i,6) ) ) & ks1 . 1 is_expressible_by n & ks1 . 2 is_expressible_by n & ks1 . 3 is_expressible_by n & ks1 . 4 is_expressible_by n & ks2 . 1 = INV_MOD ((ks1 . 1),n) & ks2 . 2 = NEG_MOD ((ks1 . 2),n) & ks2 . 3 = NEG_MOD ((ks1 . 3),n) & ks2 . 4 = INV_MOD ((ks1 . 4),n) & ke1 . 1 is_expressible_by n & ke1 . 2 is_expressible_by n & ke1 . 3 is_expressible_by n & ke1 . 4 is_expressible_by n & ke2 . 1 = INV_MOD ((ke1 . 1),n) & ke2 . 2 = NEG_MOD ((ke1 . 2),n) & ke2 . 3 = NEG_MOD ((ke1 . 3),n) & ke2 . 4 = INV_MOD ((ke1 . 4),n) & ke2 . 5 = ke1 . 5 & ke2 . 6 = ke1 . 6 holds
((IDEA_QS (ks2,n)) * ((compose ((IDEA_Q_F (Key2,n,r)),MESSAGES)) * ((IDEA_QE (ke2,n)) * ((IDEA_PE (ke1,n)) * ((compose ((IDEA_P_F (Key1,n,r)),MESSAGES)) * (IDEA_PS (ks1,n))))))) . m = m
let m be FinSequence of NAT ; ( lk >= r & (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 & ( for i being Nat st i <= r holds
( Key1 * (i,1) is_expressible_by n & Key1 * (i,2) is_expressible_by n & Key1 * (i,3) is_expressible_by n & Key1 * (i,4) is_expressible_by n & Key1 * (i,5) is_expressible_by n & Key1 * (i,6) is_expressible_by n & Key2 * (i,1) is_expressible_by n & Key2 * (i,2) is_expressible_by n & Key2 * (i,3) is_expressible_by n & Key2 * (i,4) is_expressible_by n & Key2 * (i,5) is_expressible_by n & Key2 * (i,6) is_expressible_by n & Key2 * (i,1) = INV_MOD ((Key1 * (i,1)),n) & Key2 * (i,2) = NEG_MOD ((Key1 * (i,3)),n) & Key2 * (i,3) = NEG_MOD ((Key1 * (i,2)),n) & Key2 * (i,4) = INV_MOD ((Key1 * (i,4)),n) & Key1 * (i,5) = Key2 * (i,5) & Key1 * (i,6) = Key2 * (i,6) ) ) & ks1 . 1 is_expressible_by n & ks1 . 2 is_expressible_by n & ks1 . 3 is_expressible_by n & ks1 . 4 is_expressible_by n & ks2 . 1 = INV_MOD ((ks1 . 1),n) & ks2 . 2 = NEG_MOD ((ks1 . 2),n) & ks2 . 3 = NEG_MOD ((ks1 . 3),n) & ks2 . 4 = INV_MOD ((ks1 . 4),n) & ke1 . 1 is_expressible_by n & ke1 . 2 is_expressible_by n & ke1 . 3 is_expressible_by n & ke1 . 4 is_expressible_by n & ke2 . 1 = INV_MOD ((ke1 . 1),n) & ke2 . 2 = NEG_MOD ((ke1 . 2),n) & ke2 . 3 = NEG_MOD ((ke1 . 3),n) & ke2 . 4 = INV_MOD ((ke1 . 4),n) & ke2 . 5 = ke1 . 5 & ke2 . 6 = ke1 . 6 implies ((IDEA_QS (ks2,n)) * ((compose ((IDEA_Q_F (Key2,n,r)),MESSAGES)) * ((IDEA_QE (ke2,n)) * ((IDEA_PE (ke1,n)) * ((compose ((IDEA_P_F (Key1,n,r)),MESSAGES)) * (IDEA_PS (ks1,n))))))) . m = m )
assume that
A1:
lk >= r
and
A2:
(2 to_power n) + 1 is prime
and
A3:
len m >= 4
and
A4:
( m . 1 is_expressible_by n & m . 2 is_expressible_by n & m . 3 is_expressible_by n & m . 4 is_expressible_by n )
and
A5:
for i being Nat st i <= r holds
( Key1 * (i,1) is_expressible_by n & Key1 * (i,2) is_expressible_by n & Key1 * (i,3) is_expressible_by n & Key1 * (i,4) is_expressible_by n & Key1 * (i,5) is_expressible_by n & Key1 * (i,6) is_expressible_by n & Key2 * (i,1) is_expressible_by n & Key2 * (i,2) is_expressible_by n & Key2 * (i,3) is_expressible_by n & Key2 * (i,4) is_expressible_by n & Key2 * (i,5) is_expressible_by n & Key2 * (i,6) is_expressible_by n & Key2 * (i,1) = INV_MOD ((Key1 * (i,1)),n) & Key2 * (i,2) = NEG_MOD ((Key1 * (i,3)),n) & Key2 * (i,3) = NEG_MOD ((Key1 * (i,2)),n) & Key2 * (i,4) = INV_MOD ((Key1 * (i,4)),n) & Key1 * (i,5) = Key2 * (i,5) & Key1 * (i,6) = Key2 * (i,6) )
and
A6:
( ks1 . 1 is_expressible_by n & ks1 . 2 is_expressible_by n & ks1 . 3 is_expressible_by n & ks1 . 4 is_expressible_by n & ks2 . 1 = INV_MOD ((ks1 . 1),n) & ks2 . 2 = NEG_MOD ((ks1 . 2),n) & ks2 . 3 = NEG_MOD ((ks1 . 3),n) & ks2 . 4 = INV_MOD ((ks1 . 4),n) )
and
A7:
( ke1 . 1 is_expressible_by n & ke1 . 2 is_expressible_by n & ke1 . 3 is_expressible_by n & ke1 . 4 is_expressible_by n & ke2 . 1 = INV_MOD ((ke1 . 1),n) & ke2 . 2 = NEG_MOD ((ke1 . 2),n) & ke2 . 3 = NEG_MOD ((ke1 . 3),n) & ke2 . 4 = INV_MOD ((ke1 . 4),n) & ke2 . 5 = ke1 . 5 & ke2 . 6 = ke1 . 6 )
; ((IDEA_QS (ks2,n)) * ((compose ((IDEA_Q_F (Key2,n,r)),MESSAGES)) * ((IDEA_QE (ke2,n)) * ((IDEA_PE (ke1,n)) * ((compose ((IDEA_P_F (Key1,n,r)),MESSAGES)) * (IDEA_PS (ks1,n))))))) . m = m
A8:
m in MESSAGES
by FINSEQ_1:def 11;
then
(IDEA_PS (ks1,n)) . m in MESSAGES
by FUNCT_2:5;
then reconsider m1 = (IDEA_PS (ks1,n)) . m as FinSequence of NAT by FINSEQ_1:def 11;
A9:
m1 in MESSAGES
by FINSEQ_1:def 11;
A10: len m1 =
len (IDEAoperationA (m,ks1,n))
by Def19
.=
len m
by Def11
;
m1 . 4 = (IDEAoperationA (m,ks1,n)) . 4
by Def19;
then A11:
m1 . 4 is_expressible_by n
by A3, Th26;
m1 . 3 = (IDEAoperationA (m,ks1,n)) . 3
by Def19;
then A12:
m1 . 3 is_expressible_by n
by A3, Th26;
m1 . 2 = (IDEAoperationA (m,ks1,n)) . 2
by Def19;
then A13:
m1 . 2 is_expressible_by n
by A3, Th26;
m1 . 1 = (IDEAoperationA (m,ks1,n)) . 1
by Def19;
then A14:
m1 . 1 is_expressible_by n
by A3, Th26;
per cases
( r = 0 or r <> 0 )
;
suppose A15:
r = 0
;
((IDEA_QS (ks2,n)) * ((compose ((IDEA_Q_F (Key2,n,r)),MESSAGES)) * ((IDEA_QE (ke2,n)) * ((IDEA_PE (ke1,n)) * ((compose ((IDEA_P_F (Key1,n,r)),MESSAGES)) * (IDEA_PS (ks1,n))))))) . m = mthen
len (IDEA_Q_F (Key2,n,r)) = 0
by Def18;
then A16:
IDEA_Q_F (
Key2,
n,
r)
= {}
;
len (IDEA_P_F (Key1,n,r)) = 0
by A15, Def17;
then
IDEA_P_F (
Key1,
n,
r)
= {}
;
hence ((IDEA_QS (ks2,n)) * ((compose ((IDEA_Q_F (Key2,n,r)),MESSAGES)) * ((IDEA_QE (ke2,n)) * ((IDEA_PE (ke1,n)) * ((compose ((IDEA_P_F (Key1,n,r)),MESSAGES)) * (IDEA_PS (ks1,n))))))) . m =
((IDEA_QS (ks2,n)) * ((compose ({},MESSAGES)) * ((IDEA_QE (ke2,n)) * ((IDEA_PE (ke1,n)) * ((compose ({},MESSAGES)) * (IDEA_PS (ks1,n))))))) . m
by A16
.=
((IDEA_QS (ks2,n)) * ((id MESSAGES) * ((IDEA_QE (ke2,n)) * ((IDEA_PE (ke1,n)) * ((compose ({},MESSAGES)) * (IDEA_PS (ks1,n))))))) . m
by FUNCT_7:39
.=
((IDEA_QS (ks2,n)) * ((id MESSAGES) * ((IDEA_QE (ke2,n)) * ((IDEA_PE (ke1,n)) * ((id MESSAGES) * (IDEA_PS (ks1,n))))))) . m
by FUNCT_7:39
.=
((IDEA_QS (ks2,n)) * ((IDEA_QE (ke2,n)) * ((IDEA_PE (ke1,n)) * ((id MESSAGES) * (IDEA_PS (ks1,n)))))) . m
by FUNCT_2:17
.=
((IDEA_QS (ks2,n)) * ((IDEA_QE (ke2,n)) * ((IDEA_PE (ke1,n)) * (IDEA_PS (ks1,n))))) . m
by FUNCT_2:17
.=
(IDEA_QS (ks2,n)) . (((IDEA_QE (ke2,n)) * ((IDEA_PE (ke1,n)) * (IDEA_PS (ks1,n)))) . m)
by A8, FUNCT_2:15
.=
(IDEA_QS (ks2,n)) . ((IDEA_QE (ke2,n)) . (((IDEA_PE (ke1,n)) * (IDEA_PS (ks1,n))) . m))
by A8, FUNCT_2:15
.=
(IDEA_QS (ks2,n)) . ((IDEA_QE (ke2,n)) . ((IDEA_PE (ke1,n)) . m1))
by A8, FUNCT_2:15
.=
(IDEA_QS (ks2,n)) . (((IDEA_QE (ke2,n)) * (IDEA_PE (ke1,n))) . m1)
by A9, FUNCT_2:15
.=
(IDEA_QS (ks2,n)) . ((IDEA_PS (ks1,n)) . m)
by A2, A3, A7, A10, A14, A13, A12, A11, Th35
.=
((IDEA_QS (ks2,n)) * (IDEA_PS (ks1,n))) . m
by A8, FUNCT_2:15
.=
m
by A2, A3, A4, A6, Th34
;
verum end; suppose A17:
r <> 0
;
((IDEA_QS (ks2,n)) * ((compose ((IDEA_Q_F (Key2,n,r)),MESSAGES)) * ((IDEA_QE (ke2,n)) * ((IDEA_PE (ke1,n)) * ((compose ((IDEA_P_F (Key1,n,r)),MESSAGES)) * (IDEA_PS (ks1,n))))))) . m = mthen A18:
IDEA_P_F (
Key1,
n,
r) is
FuncSequence of
MESSAGES ,
MESSAGES
by Th40;
then A19:
firstdom (IDEA_P_F (Key1,n,r)) = MESSAGES
by FUNCT_7:def 9;
then A20:
dom (compose ((IDEA_P_F (Key1,n,r)),MESSAGES)) = MESSAGES
by A18, FUNCT_7:62;
(
IDEA_P_F (
Key1,
n,
r)
= {} implies
rng (compose ((IDEA_P_F (Key1,n,r)),MESSAGES)) = {} )
by A19, FUNCT_7:def 6;
then A21:
rng (compose ((IDEA_P_F (Key1,n,r)),MESSAGES)) c= lastrng (IDEA_P_F (Key1,n,r))
by FUNCT_7:59, XBOOLE_1:2;
lastrng (IDEA_P_F (Key1,n,r)) c= MESSAGES
by A18, FUNCT_7:def 9;
then
rng (compose ((IDEA_P_F (Key1,n,r)),MESSAGES)) c= MESSAGES
by A21, XBOOLE_1:1;
then reconsider PF =
compose (
(IDEA_P_F (Key1,n,r)),
MESSAGES) as
Function of
MESSAGES,
MESSAGES by A20, FUNCT_2:def 1, RELSET_1:4;
A22:
rng PF c= MESSAGES
by RELAT_1:def 19;
PF . m1 in MESSAGES
by A9, FUNCT_2:5;
then reconsider m2 =
PF . m1 as
FinSequence of
NAT by FINSEQ_1:def 11;
A23:
(
len m2 >= 4 &
m2 . 1
is_expressible_by n )
by A3, A10, A14, A13, A12, A11, Th45;
A24:
IDEA_Q_F (
Key2,
n,
r) is
FuncSequence of
MESSAGES ,
MESSAGES
by A17, Th41;
then A25:
firstdom (IDEA_Q_F (Key2,n,r)) = MESSAGES
by FUNCT_7:def 9;
then A26:
dom (compose ((IDEA_Q_F (Key2,n,r)),MESSAGES)) = MESSAGES
by A24, FUNCT_7:62;
(
IDEA_Q_F (
Key2,
n,
r)
= {} implies
rng (compose ((IDEA_Q_F (Key2,n,r)),MESSAGES)) = {} )
by A25, FUNCT_7:def 6;
then A27:
rng (compose ((IDEA_Q_F (Key2,n,r)),MESSAGES)) c= lastrng (IDEA_Q_F (Key2,n,r))
by FUNCT_7:59, XBOOLE_1:2;
lastrng (IDEA_Q_F (Key2,n,r)) c= MESSAGES
by A24, FUNCT_7:def 9;
then
rng (compose ((IDEA_Q_F (Key2,n,r)),MESSAGES)) c= MESSAGES
by A27, XBOOLE_1:1;
then reconsider QF =
compose (
(IDEA_Q_F (Key2,n,r)),
MESSAGES) as
Function of
MESSAGES,
MESSAGES by A26, FUNCT_2:def 1, RELSET_1:4;
A28:
m2 in MESSAGES
by FINSEQ_1:def 11;
A29:
QF . (PF . m1) =
(QF * PF) . m1
by A9, FUNCT_2:15
.=
(compose (((IDEA_P_F (Key1,n,r)) ^ (IDEA_Q_F (Key2,n,r))),MESSAGES)) . m1
by A22, FUNCT_7:48
.=
m1
by A1, A2, A3, A5, A10, A14, A13, A12, A11, Th46
;
A30:
m2 . 4
is_expressible_by n
by A3, A10, A14, A13, A12, A11, Th45;
A31:
(
m2 . 2
is_expressible_by n &
m2 . 3
is_expressible_by n )
by A3, A10, A14, A13, A12, A11, Th45;
thus ((IDEA_QS (ks2,n)) * ((compose ((IDEA_Q_F (Key2,n,r)),MESSAGES)) * ((IDEA_QE (ke2,n)) * ((IDEA_PE (ke1,n)) * ((compose ((IDEA_P_F (Key1,n,r)),MESSAGES)) * (IDEA_PS (ks1,n))))))) . m =
(IDEA_QS (ks2,n)) . ((QF * ((IDEA_QE (ke2,n)) * ((IDEA_PE (ke1,n)) * (PF * (IDEA_PS (ks1,n)))))) . m)
by A8, FUNCT_2:15
.=
(IDEA_QS (ks2,n)) . (QF . (((IDEA_QE (ke2,n)) * ((IDEA_PE (ke1,n)) * (PF * (IDEA_PS (ks1,n))))) . m))
by A8, FUNCT_2:15
.=
(IDEA_QS (ks2,n)) . (QF . ((IDEA_QE (ke2,n)) . (((IDEA_PE (ke1,n)) * (PF * (IDEA_PS (ks1,n)))) . m)))
by A8, FUNCT_2:15
.=
(IDEA_QS (ks2,n)) . (QF . ((IDEA_QE (ke2,n)) . ((IDEA_PE (ke1,n)) . ((PF * (IDEA_PS (ks1,n))) . m))))
by A8, FUNCT_2:15
.=
(IDEA_QS (ks2,n)) . (QF . ((IDEA_QE (ke2,n)) . ((IDEA_PE (ke1,n)) . (PF . ((IDEA_PS (ks1,n)) . m)))))
by A8, FUNCT_2:15
.=
(IDEA_QS (ks2,n)) . (QF . (((IDEA_QE (ke2,n)) * (IDEA_PE (ke1,n))) . m2))
by A28, FUNCT_2:15
.=
(IDEA_QS (ks2,n)) . m1
by A2, A7, A23, A31, A30, A29, Th35
.=
((IDEA_QS (ks2,n)) * (IDEA_PS (ks1,n))) . m
by A8, FUNCT_2:15
.=
m
by A2, A3, A4, A6, Th34
;
verum end; end;