let f, g be ManySortedSet of ; :: thesis: ( support f = X /\ SCNAT & ( for k being Element of NAT st k in support f holds
f . k = Moebius k ) & support g = X /\ SCNAT & ( for k being Element of NAT st k in support g holds
g . k = Moebius k ) implies f = g )
assume that
A11: ( support f = X /\ SCNAT & ( for k being Element of NAT st k in support f holds
f . k = Moebius k ) ) and
A12: ( support g = X /\ SCNAT & ( for k being Element of NAT st k in support g holds
g . k = Moebius k ) ) ; :: thesis: f = g
for i being set st i in NAT holds
f . i = g . i

proof

let i be set ; :: thesis: ( i in NAT implies f . i = g . i )
assume i in NAT ; :: thesis: f . i = g . i
then reconsider j = i as Element of NAT ;

per cases ( j in support f or not j in support f ) ;

suppose A13: j in support f ; :: thesis: f . i = g . i

hence f . i = Moebius j by A11
.= g . i by A11, A12, A13 ;
:: thesis: verum

end;

suppose A14: not j in support f ; :: thesis: f . i = g . i

hence f . i = 0 by POLYNOM1:def 7
.= g . i by A11, A12, A14, POLYNOM1:def 7 ;
:: thesis: verum

end;

end;

end;

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