let s be Nat; :: thesis: ( s >= 2 implies for f being s -element real-valued positive-yielding FinSequence st f is with_sum_of_reciprocals_equal_1 holds
for k being Nat st k in dom f holds
f . k > 1 )
assume A1: s >= 2 ; :: thesis: for f being s -element real-valued positive-yielding FinSequence st f is with_sum_of_reciprocals_equal_1 holds
for k being Nat st k in dom f holds
f . k > 1
let f be s -element real-valued positive-yielding FinSequence; :: thesis: ( f is with_sum_of_reciprocals_equal_1 implies for k being Nat st k in dom f holds
f . k > 1 )
assume A2: f is with_sum_of_reciprocals_equal_1 ; :: thesis: for k being Nat st k in dom f holds
f . k > 1
let k be Nat; :: thesis: ( k in dom f implies f . k > 1 )
assume A3: k in dom f ; :: thesis: f . k > 1
A4: dom f = dom (f ") by VALUED_1:def 7;
len (f ") = s by CARD_1:def 7;
then A5: (f ") . k < 1 by A1, A2, A3, A4, Th42;
(f ") . k = (f . k) " by VALUED_1:10;
then 1 " < ((f . k) ") " by A3, A5, XREAL_1:85, RVSUM_3:def 1;
hence f . k > 1 ; :: thesis: verum