let T be NormedLinearTopSpace; :: thesis: ( T is compact implies T is complete )
assume T is compact ; :: thesis: T is complete
then TopSpaceNorm T is compact by Th20;
then MetricSpaceNorm T is sequentially_compact by TOPMETR4:11;
hence T is complete by Th6, TOPMETR4:12; :: thesis: verum