let F, G be ManySortedFunction of (product A),(A . i); ( ( for s being Element of S holds F . s = proj ((Carrier (A,s)),i) ) & ( for s being Element of S holds G . s = proj ((Carrier (A,s)),i) ) implies F = G )
assume that
A8:
for s being Element of S holds F . s = proj ((Carrier (A,s)),i)
and
A9:
for s being Element of S holds G . s = proj ((Carrier (A,s)),i)
; F = G
hence
F = G
; verum