let f, g be ManySortedSet of ; :: thesis: ( ( for i being set holds f . i = a * (b . i) ) & ( for i being set holds g . i = a * (b . i) ) implies f = g )
assume that
A4: for i being set holds f . i = a * (b . i) and
A5: for i being set holds g . i = a * (b . i) ; :: thesis: f = g
for i being set st i in X holds
f . i = g . i

proof

let i be set ; :: thesis: ( i in X implies f . i = g . i )
assume i in X ; :: thesis: f . i = g . i
thus f . i = a * (b . i) by A4
.= g . i by A5 ; :: thesis: verum

end;

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