defpred S_{1}[ 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_{1}[e,u]

A2: for e being Element of MESSAGES holds S_{1}[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

( $1 = F & $2 = IDEAoperationA (F,k,n) );

A1: for e being Element of MESSAGES ex u being Element of MESSAGES st S

proof

consider m1 being Function of MESSAGES,MESSAGES such that
let e be Element of MESSAGES ; :: thesis: ex u being Element of MESSAGES st S_{1}[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_{1}[e,u]

thus S_{1}[e,u]
; :: thesis: verum

end;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

thus S

A2: for e being Element of MESSAGES holds S

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