let M, N be ManySortedFunction of A,C; :: thesis: ( ( 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) ; :: thesis: M = N

now :: thesis: for i being object st i in I holds
M . i = N . i

let i be object ; :: thesis: ( i in I implies M . i = N . i )
assume A24: i in I ; :: thesis: M . i = N . i
hence M . i = pr2 (F . i) by A22
.= N . i by A23, A24 ;
:: thesis: verum

end;

hence M = N ; :: thesis: verum