let f, g be ManySortedSet of the carrier of S; :: 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 object st x in the carrier of S holds
f . x = g . x

proof

let x be object ; :: 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)) by A2;
hence f . x = g . x by A3; :: thesis: verum

end;

hence f = g ; :: thesis: verum