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

proof

A6: ( dom m1 = MESSAGES & dom m2 = MESSAGES ) by FUNCT_2:def 1;

now

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

end;

hence m1 = m2 by A6, FUNCT_1:9; :: thesis: verum

end;

hence m1 = m2 ; :: thesis: verum