let f, g be ManySortedSet of X; ( ( for i being object holds f . i = a * (b . i) ) & ( for i being object holds g . i = a * (b . i) ) implies f = g )
assume that
A4:
for i being object holds f . i = a * (b . i)
and
A5:
for i being object holds g . i = a * (b . i)
; f = g
for i being object st i in X holds
f . i = g . i
proof
let i be
object ;
( i in X implies f . i = g . i )
assume
i in X
;
f . i = g . i
thus f . i =
a * (b . i)
by A4
.=
g . i
by A5
;
verum
end;
hence
f = g
; verum