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