let v be Element of (REAL-NS 1); :: thesis: abs ((proj 1,1) . v) = ||.v.||
reconsider x = (proj 1,1) . v as Real ;
reconsider w = v as Element of REAL 1 by REAL_NS1:def 4;
( len w = 1 & w . 1 = x ) by FINSEQ_1:def 18, PDIFF_1:def 1;
then <*x*> = w by FINSEQ_1:57;
hence abs ((proj 1,1) . v) = ||.v.|| by Lm21; :: thesis: verum