let f, g be ManySortedSet of ; :: thesis: ( ( for s being SortSymbol of S holds f . s = product (Carrier A,s) ) & ( for s being SortSymbol of S holds g . s = product (Carrier A,s) ) implies f = g )
assume that
A2: for s being SortSymbol of S holds f . s = product (Carrier A,s) and
A3: for s being SortSymbol of S holds g . s = product (Carrier A,s) ; :: thesis: f = g
for x being set st x in the carrier of S holds
f . x = g . x

proof

let x be set ; :: thesis: ( x in the carrier of S implies f . x = g . x )
assume x in the carrier of S ; :: thesis: f . x = g . x
then reconsider x1 = x as SortSymbol of S ;
( f . x1 = product (Carrier A,x1) & g . x1 = product (Carrier A,x1) ) by A2, A3;
hence f . x = g . x ; :: thesis: verum

end;

hence f = g by PBOOLE:3; :: thesis: verum