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
A14: for i being set st i in I holds
M . i = pr1 (F . i) and
A15: for i being set st i in I holds
N . i = pr1 (F . i) ; :: thesis: M = N

now

let i be set ; :: thesis: ( i in I implies M . i = N . i )
assume A16: i in I ; :: thesis: M . i = N . i
hence M . i = pr1 (F . i) by A14
.= N . i by A15, A16 ;
:: thesis: verum

end;

hence M = N by PBOOLE:3; :: thesis: verum