take NAT --> 0c ; :: thesis: NAT --> 0c is summable
take 0c ; :: according to COMSEQ_2:def 4,COMSEQ_3:def 10 :: thesis: for b₁ being Element of REAL holds
( b₁ <= 0 or ex b₂ being Element of NAT st
for b₃ being Element of NAT holds
( not b₂ <= b₃ or not b₁ <= |.(((Partial_Sums (NAT --> 0c )) . b₃) - 0c ).| ) )
let p be Real; :: thesis: ( p <= 0 or ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not p <= |.(((Partial_Sums (NAT --> 0c )) . b₂) - 0c ).| ) )
assume A1: 0 < p ; :: thesis: ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not p <= |.(((Partial_Sums (NAT --> 0c )) . b₂) - 0c ).| )
take 0 ; :: thesis: for b₁ being Element of NAT holds
( not 0 <= b₁ or not p <= |.(((Partial_Sums (NAT --> 0c )) . b₁) - 0c ).| )
for n being Element of NAT holds (NAT --> 0c ) . n = 0c by FUNCOP_1:13;
hence for b₁ being Element of NAT holds
( not 0 <= b₁ or not p <= |.(((Partial_Sums (NAT --> 0c )) . b₁) - 0c ).| ) by A1, Th24, COMPLEX1:130; :: thesis: verum