defpred S1[ set , set ] means ex F being FinSequence of NAT st
( $1 = F & $2 = IDEAoperationA (F,k,n) );
A1:
for e being Element of MESSAGES ex u being Element of MESSAGES st S1[e,u]
consider m1 being Function of MESSAGES,MESSAGES such that
A2:
for e being Element of MESSAGES holds S1[e,m1 . e]
from FUNCT_2:sch 3(A1);
take
m1
; for m being FinSequence of NAT holds m1 . m = IDEAoperationA (m,k,n)
let m be FinSequence of NAT ; m1 . m = IDEAoperationA (m,k,n)
m is Element of MESSAGES
by FINSEQ_1:def 11;
then
ex F being FinSequence of NAT st
( m = F & m1 . m = IDEAoperationA (F,k,n) )
by A2;
hence
m1 . m = IDEAoperationA (m,k,n)
; verum