let f be FinSequence of NAT ; :: thesis: for p being Prime st Product f <> 0 holds
p |-count (Product f) = Sum (p |-count f)
defpred S₁[ Nat] means for f being FinSequence of NAT
for p being Prime st $1 = len f & Product f <> 0 holds
p |-count (Product f) = Sum (p |-count f);
let p be Prime; :: thesis: ( Product f <> 0 implies p |-count (Product f) = Sum (p |-count f) )
assume A1: Product f <> 0 ; :: thesis: p |-count (Product f) = Sum (p |-count f)
A2: ex n being Element of NAT st n = len f ;
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
for f being FinSequence of NAT
for p being Prime st n + 1 = len f & Product f <> 0 holds
p |-count (Product f) = Sum (p |-count f)

proof

let f be FinSequence of NAT ; :: thesis: for p being Prime st n + 1 = len f & Product f <> 0 holds
p |-count (Product f) = Sum (p |-count f)
let p be Prime; :: thesis: ( n + 1 = len f & Product f <> 0 implies p |-count (Product f) = Sum (p |-count f) )
assume that
A5: n + 1 = len f and
A6: Product f <> 0 ; :: thesis: p |-count (Product f) = Sum (p |-count f)
consider g being FinSequence of NAT , d being Element of NAT such that
A7: f = g ^ <*d*> by A5, FINSEQ_2:19;
len f = (len g) + (len <*d*>) by A7, FINSEQ_1:22;
then A8: n + 1 = (len g) + 1 by A5, FINSEQ_1:39;
A9: (Product g) * d <> 0 by A6, A7, RVSUM_1:96;
then A10: Product g <> 0 ;
A11: d <> 0 by A9;
p |-count (Product f) = p |-count ((Product g) * d) by A7, RVSUM_1:96
.= (p |-count (Product g)) + (p |-count d) by A10, A11, NAT_3:28
.= (Sum (p |-count g)) + (p |-count d) by A4, A10, A8
.= Sum ((p |-count g) ^ <*(p |-count d)*>) by RVSUM_1:74
.= Sum ((p |-count g) ^ (p |-count <*d*>)) by A11, Th51
.= Sum (p |-count (g ^ <*d*>)) by Th50 ;
hence p |-count (Product f) = Sum (p |-count f) by A7; :: thesis: verum

end;

hence S₁[n + 1] ; :: thesis: verum

end;

A12: S₁[ 0 ]

proof

let f be FinSequence of NAT ; :: thesis: for p being Prime st 0 = len f & Product f <> 0 holds
p |-count (Product f) = Sum (p |-count f)
let p be Prime; :: thesis: ( 0 = len f & Product f <> 0 implies p |-count (Product f) = Sum (p |-count f) )
assume that
A13: 0 = len f and
Product f <> 0 ; :: thesis: p |-count (Product f) = Sum (p |-count f)
A14: p <> 1 by INT_2:def 4;
A15: f = {} by A13;
then Sum (p |-count f) = 0 by Th49, RVSUM_1:72;
hence p |-count (Product f) = Sum (p |-count f) by A15, A14, NAT_3:21, RVSUM_1:94; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A12, A3);
hence p |-count (Product f) = Sum (p |-count f) by A1, A2; :: thesis: verum