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

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