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

proof

let i be object ; :: 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 A14: j in support f ; :: thesis: f . i = g . i

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

end;

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

hence f . i = 0 by PRE_POLY:def 7
.= g . i by A10, A12, A15, PRE_POLY:def 7 ;
:: thesis: verum

end;

end;

end;

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