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
A11: for s being Element of S holds F . s = proj (Carrier A,s),i and
A12: for s being Element of S holds G . s = proj (Carrier A,s),i ; :: thesis: F = G

now

let s' be set ; :: thesis: ( s' in the carrier of S implies F . s' = G . s' )
assume s' in the carrier of S ; :: thesis: F . s' = G . s'
then reconsider s'' = s' as Element of S ;
thus F . s' = proj (Carrier A,s''),i by A11
.= G . s' by A12 ; :: thesis: verum

end;

hence F = G by PBOOLE:3; :: thesis: verum