let F, G be ManySortedFunction of ,(product A); :: thesis: ( ( for s being Element of holds F . s = proj (Carrier A,s),i ) & ( for s being Element of holds G . s = proj (Carrier A,s),i ) implies F = G )
assume that
A8: for s being Element of holds F . s = proj (Carrier A,s),i and
A9: for s being Element of 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 ;
thus F . s' = proj (Carrier A,s''),i by A8
.= G . s' by A9 ; :: thesis: verum

end;

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