let m1, m2 be Function of MESSAGES,MESSAGES; ( ( for m being FinSequence of NAT holds m1 . m = IDEAoperationA ((IDEAoperationC (IDEAoperationB (m,k,n))),k,n) ) & ( for m being FinSequence of NAT holds m2 . m = IDEAoperationA ((IDEAoperationC (IDEAoperationB (m,k,n))),k,n) ) implies m1 = m2 )
assume that
A3:
for m being FinSequence of NAT holds m1 . m = IDEAoperationA ((IDEAoperationC (IDEAoperationB (m,k,n))),k,n)
and
A4:
for m being FinSequence of NAT holds m2 . m = IDEAoperationA ((IDEAoperationC (IDEAoperationB (m,k,n))),k,n)
; m1 = m2
( dom m1 = MESSAGES & dom m2 = MESSAGES )
by FUNCT_2:def 1;
hence
m1 = m2
by A5, FUNCT_1:2; verum