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