let v be Element of (REAL-NS 1); :: thesis: |.((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 CARD_1:def 7, PDIFF_1:def 1;
then <*x*> = w by FINSEQ_1:40;
hence |.((proj (1,1)) . v).| = ||.v.|| by Lm20; :: thesis: verum