let s, s' be Complex_Sequence; :: thesis: ( s is convergent & s' is convergent implies lim |.(s - s').| = |.((lim s) - (lim s')).| )
assume A1: ( s is convergent & s' is convergent ) ; :: thesis: lim |.(s - s').| = |.((lim s) - (lim s')).|
then s - s' is convergent by Th25;
hence lim |.(s - s').| = |.(lim (s - s')).| by Th11
.= |.((lim s) - (lim s')).| by A1, Th26 ;
:: thesis: verum