let M, N be ManySortedFunction of A,C; ( ( for i being set st i in I holds
M . i = pr2 (F . i) ) & ( for i being set st i in I holds
N . i = pr2 (F . i) ) implies M = N )
assume that
A22:
for i being set st i in I holds
M . i = pr2 (F . i)
and
A23:
for i being set st i in I holds
N . i = pr2 (F . i)
; M = N
hence
M = N
; verum