let A be non empty closed_interval Subset of REAL; :: thesis: ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 )
now :: thesis: ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 )
per cases ( vol A <> 0 or vol A = 0 ) ;
suppose A1: vol A <> 0 ; :: thesis: ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 )
vol A >= 0 by INTEGRA1:9;
hence ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 ) by A1, Lm5; :: thesis: verum
end;
suppose vol A = 0 ; :: thesis: ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 )
hence ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 ) by Lm6; :: thesis: verum
end;
end;
end;
hence ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 ) ; :: thesis: verum