let x be Real; :: thesis: for y being Element of REAL 1 st <*x*> = y holds
|.x.| = |.y.|
let y be Element of REAL 1; :: thesis: ( <*x*> = y implies |.x.| = |.y.| )
assume A1: <*x*> = y ; :: thesis: |.x.| = |.y.|
reconsider I = (proj (1,1)) " as Function of REAL,(REAL 1) by PDIFF_1:2;
reconsider y0 = y as Point of (REAL-NS 1) by REAL_NS1:def 4;
I . x = y by A1, PDIFF_1:1;
then |.x.| = ||.y0.|| by PDIFF_1:3;
hence |.x.| = |.y.| by REAL_NS1:1; :: thesis: verum