let X be RealNormSpace; :: 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 ; :: thesis: verum

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 ; :: thesis: verum