let F, G be ManySortedFunction of (product A),(A . i); :: thesis: ( ( for s being Element of S holds F . s = proj ((Carrier (A,s)),i) ) & ( for s being Element of S holds G . s = proj ((Carrier (A,s)),i) ) implies F = G )
assume that
A8: for s being Element of S holds F . s = proj ((Carrier (A,s)),i) and
A9: for s being Element of S holds G . s = proj ((Carrier (A,s)),i) ; :: thesis: F = G

now :: thesis: for s9 being object st s9 in the carrier of S holds
F . s9 = G . s9

let s9 be object ; :: thesis: ( s9 in the carrier of S implies F . s9 = G . s9 )
assume s9 in the carrier of S ; :: thesis: F . s9 = G . s9
then reconsider s99 = s9 as Element of S ;
thus F . s9 = proj ((Carrier (A,s99)),i) by A8
.= G . s9 by A9 ; :: thesis: verum

end;

hence F = G ; :: thesis: verum