let X be ComplexNormSpace; :: thesis: for seq being sequence of X
for m being Nat holds 0 <= ||.seq.|| . m
let seq be sequence of X; :: thesis: for m being Nat holds 0 <= ||.seq.|| . m
let m be Nat; :: thesis: 0 <= ||.seq.|| . m
||.seq.|| . m = ||.(seq . m).|| by NORMSP_0:def 4;
hence 0 <= ||.seq.|| . m by CLVECT_1:105; :: thesis: verum