let m be natural-valued finite-support ManySortedSet of SetPrimes ; :: thesis: for p being Prime st support m = {p} holds
Product m = m . p
let p be Prime; :: thesis: ( support m = {p} implies Product m = m . p )
assume A1: support m = {p} ; :: thesis: Product m = m . p
consider f being FinSequence of COMPLEX such that
A15: Product m = Product f and
A16: f = m * (canFS (support m)) by NAT_3:def 5;
Z1: m * <*p*> = <*(m . p)*>
proof
D1: rng <*p*> = {p} by FINSEQ_1:39;
d2: p in SetPrimes by NEWTON:def 6;
dom m = SetPrimes by PARTFUN1:def 2;
then B1: dom (m * <*p*>) = dom <*p*> by D1, d2, RELAT_1:27, ZFMISC_1:31
.= Seg 1 by FINSEQ_1:38 ;
B2: dom (m * <*p*>) = dom <*(m . p)*> by B1, FINSEQ_1:38;
for x being object st x in dom (m * <*p*>) holds
(m * <*p*>) . x = <*(m . p)*> . x
proof
let x be object ; :: thesis: ( x in dom (m * <*p*>) implies (m * <*p*>) . x = <*(m . p)*> . x )
assume C1: x in dom (m * <*p*>) ; :: thesis: (m * <*p*>) . x = <*(m . p)*> . x
then C2: x = 1 by B1, TARSKI:def 1, FINSEQ_1:2;
then (m * <*p*>) . x = m . (<*p*> . 1) by FUNCT_1:12, C1
.= <*(m . p)*> . x by C2 ;
hence (m * <*p*>) . x = <*(m . p)*> . x ; :: thesis: verum
end;
hence m * <*p*> = <*(m . p)*> by B2, FUNCT_1:2; :: thesis: verum
end;
f = <*(m . p)*> by Z1, FINSEQ_1:94, A16, A1;
hence Product m = m . p by RVSUM_1:95, A15; :: thesis: verum