defpred S₁[ 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 S₁[e,u]

proof

let e be Element of MESSAGES ; :: thesis: ex u being Element of MESSAGES st S₁[e,u]
reconsider F = e as FinSequence of NAT by FINSEQ_1:def 11;
reconsider u = IDEAoperationA (F,k,n) as Element of MESSAGES by FINSEQ_1:def 11;
take u ; :: thesis: S₁[e,u]
thus S₁[e,u] ; :: thesis: verum

end;

consider m1 being Function of MESSAGES,MESSAGES such that
A2: for e being Element of MESSAGES holds S₁[e,m1 . e] from FUNCT_2:sch 3(A1);
take m1 ; :: thesis: for m being FinSequence of NAT holds m1 . m = IDEAoperationA (m,k,n)
let m be FinSequence of NAT ; :: thesis: 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) ; :: thesis: verum