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

now

let i be set ; :: thesis: ( i in I implies M . i = N . i )
assume A32: i in I ; :: thesis: M . i = N . i
hence M . i = pr2 (F . i) by A30
.= N . i by A31, A32 ;
:: thesis: verum

end;

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