let M, N be ManySortedFunction of A,B; :: thesis: ( ( for i being set st i in I holds
M . i = pr1 (F . i) ) & ( for i being set st i in I holds
N . i = pr1 (F . i) ) implies M = N )
assume that
A10: for i being set st i in I holds
M . i = pr1 (F . i) and
A11: for i being set st i in I holds
N . i = pr1 (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 A12: i in I ; :: thesis: M . i = N . i
hence M . i = pr1 (F . i) by A10
.= N . i by A11, A12 ;
:: thesis: verum

end;

hence M = N ; :: thesis: verum