take NAT --> 0c ; :: thesis: NAT --> 0c is summable
take 0c ; :: according to COMSEQ_2:def 5,COMSEQ_3:def 8 :: thesis: for b₁ being object holds
( b₁ <= 0 or ex b₂ being set st
for b₃ being set holds
( not b₂ <= b₃ or not b₁ <= |.(((Partial_Sums (NAT --> 0c)) . b₃) - 0c).| ) )
let p be Real; :: thesis: ( p <= 0 or ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or not p <= |.(((Partial_Sums (NAT --> 0c)) . b₂) - 0c).| ) )
assume A1: 0 < p ; :: thesis: ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or not p <= |.(((Partial_Sums (NAT --> 0c)) . b₂) - 0c).| )
take 0 ; :: thesis: for b₁ being set holds
( not 0 <= b₁ or not p <= |.(((Partial_Sums (NAT --> 0c)) . b₁) - 0c).| )
for n being Nat holds (NAT --> 0c) . n = 0c ;
hence for b₁ being set holds
( not 0 <= b₁ or not p <= |.(((Partial_Sums (NAT --> 0c)) . b₁) - 0c).| ) by A1, Th24, COMPLEX1:44; :: thesis: verum