let m1, m2 be Function of MESSAGES,MESSAGES; :: thesis: ( ( for m being FinSequence of NAT holds m1 . m = IDEAoperationA ((IDEAoperationB (m,k,n)),k,n) ) & ( for m being FinSequence of NAT holds m2 . m = IDEAoperationA ((IDEAoperationB (m,k,n)),k,n) ) implies m1 = m2 )
assume that
A3: for m being FinSequence of NAT holds m1 . m = IDEAoperationA ((IDEAoperationB (m,k,n)),k,n) and
A4: for m being FinSequence of NAT holds m2 . m = IDEAoperationA ((IDEAoperationB (m,k,n)),k,n) ; :: thesis: m1 = m2

A5: now :: thesis: for j being object st j in MESSAGES holds
m1 . j = m2 . j

let j be object ; :: thesis: ( j in MESSAGES implies m1 . j = m2 . j )
reconsider jj = j as set by TARSKI:1;
assume j in MESSAGES ; :: thesis: m1 . j = m2 . j
then reconsider jj = jj as FinSequence of NAT by FINSEQ_1:def 11;
thus m1 . j = IDEAoperationA ((IDEAoperationB (jj,k,n)),k,n) by A3
.= m2 . j by A4 ; :: thesis: verum

end;

( dom m1 = MESSAGES & dom m2 = MESSAGES ) by FUNCT_2:def 1;
hence m1 = m2 by A5, FUNCT_1:2; :: thesis: verum