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

A5: now

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

end;

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