let n be Nat; :: thesis: for s being Real_Sequence st ( for n being Nat holds s . n > 0 ) holds
(n + 1) -root ((Partial_Product s) . n) > 0
let s be Real_Sequence; :: thesis: ( ( for n being Nat holds s . n > 0 ) implies (n + 1) -root ((Partial_Product s) . n) > 0 )
assume for n being Nat holds s . n > 0 ; :: thesis: (n + 1) -root ((Partial_Product s) . n) > 0
then A1: (Partial_Product s) . n > 0 by Th43;
A2: n + 1 >= 0 + 1 by XREAL_1:6;
then (n + 1) -root ((Partial_Product s) . n) = (n + 1) -Root ((Partial_Product s) . n) by A1, POWER:def 1;
hence (n + 1) -root ((Partial_Product s) . n) > 0 by A1, A2, PREPOWER:def 2; :: thesis: verum