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

let s9 be set ; :: 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 by PBOOLE:3; :: thesis: verum