deffunc H₁( Real) -> Element of REAL 1 = In (<*$1*>,(REAL 1));
consider f being Function of REAL,(REAL 1) such that
A1: for x being Element of REAL holds f . x = H₁(x) from FUNCT_2:sch 4();
A2: for x being Element of RNS_Real holds f . x = <*x*>

proof

let x be Element of RNS_Real; :: thesis: f . x = <*x*>
reconsider x0 = x as Element of REAL ;
f . x = In (<*x*>,(REAL 1)) by A1;
hence f . x = <*x*> by SUBSET_1:def 8; :: thesis: verum

end;

reconsider f = f as Function of the carrier of RNS_Real, the carrier of (REAL-NS 1) by REAL_NS1:def 4;
for v, w being Element of RNS_Real holds f . (v + w) = (f . v) + (f . w)

proof

let v, w be Element of RNS_Real; :: thesis: f . (v + w) = (f . v) + (f . w)
reconsider v0 = v, w0 = w as Element of REAL ;
A4: f . v = <*v0*> by A2;
A5: f . w = <*w0*> by A2;
v + w = v0 + w0 by BINOP_2:def 9;
hence f . (v + w) = <*(v0 + w0)*> by A2
.= <*v0*> + <*w0*> by RVSUM_1:13
.= (f . v) + (f . w) by A4, A5, REAL_NS1:2 ;
:: thesis: verum

end;

then A7: f is additive ;
for x being VECTOR of RNS_Real
for r being Real holds f . (r * x) = r * (f . x)

proof

let v be VECTOR of RNS_Real; :: thesis: for r being Real holds f . (r * v) = r * (f . v)
let r be Real; :: thesis: f . (r * v) = r * (f . v)
reconsider v0 = v as Element of REAL ;
r * v = r * v0 by BINOP_2:def 11;
hence f . (r * v) = <*(r * v0)*> by A2
.= r * <*v0*> by RVSUM_1:47
.= r * (f . v) by A2, REAL_NS1:3 ;
:: thesis: verum

end;

then reconsider f = f as LinearOperator of RNS_Real,(REAL-NS 1) by A7, LOPBAN_1:def 5;
take f ; :: thesis: ( f is isomorphism & ( for x being Element of RNS_Real holds f . x = <*x*> ) )

now :: thesis: for z1, z2 being object st z1 in the carrier of RNS_Real & z2 in the carrier of RNS_Real & f . z1 = f . z2 holds
z1 = z2

let z1, z2 be object ; :: thesis: ( z1 in the carrier of RNS_Real & z2 in the carrier of RNS_Real & f . z1 = f . z2 implies z1 = z2 )
assume A9: ( z1 in the carrier of RNS_Real & z2 in the carrier of RNS_Real & f . z1 = f . z2 ) ; :: thesis: z1 = z2
<*z1*> = f . z1 by A2, A9
.= <*z2*> by A2, A9 ;
hence z1 = z2 by FINSEQ_1:76; :: thesis: verum

end;

then A10: f is one-to-one by FUNCT_2:19;

now :: thesis: for w being object st w in the carrier of (REAL-NS 1) holds
w in rng f

let w be object ; :: thesis: ( w in the carrier of (REAL-NS 1) implies w in rng f )
assume w in the carrier of (REAL-NS 1) ; :: thesis: w in rng f
then w in REAL 1 by REAL_NS1:def 4;
then w in { s where s is Element of REAL * : len s = 1 } by FINSEQ_2:def 4;
then consider s being Element of REAL * such that
A11: ( w = s & len s = 1 ) ;
set x = s . 1;
A12: 1 in {1} by TARSKI:def 1;
1 in dom s by A11, A12, FINSEQ_1:2, FINSEQ_1:def 3;
then s . 1 in rng s by FUNCT_1:3;
then reconsider x = s . 1 as Element of REAL ;
reconsider x = x as Element of RNS_Real ;
A13: w = <*x*> by A11, FINSEQ_1:40;
f . x = w by A2, A13;
hence w in rng f by FUNCT_2:112; :: thesis: verum

end;

then the carrier of (REAL-NS 1) c= rng f ;
then A14: f is onto by FUNCT_2:def 3, XBOOLE_0:def 10;
for x being Point of RNS_Real holds ||.x.|| = ||.(f . x).||

proof

let x be Point of RNS_Real; :: thesis: ||.x.|| = ||.(f . x).||
reconsider x0 = x as Element of REAL ;
A15: <*x0*> in REAL 1 ;
then reconsider x1 = <*x0*> as VECTOR of (REAL-NS 1) by REAL_NS1:def 4;
||.(f . x).|| = |.<*x0*>.| by A2, REAL_NS1:1
.= ||.x1.|| by A15, REAL_NS1:1
.= |.x0.| by PDIFF_8:2
.= absreal . x0 by EUCLID:def 2
.= ||.x.|| ;
hence ||.x.|| = ||.(f . x).|| ; :: thesis: verum

end;

hence ( f is isomorphism & ( for x being Element of RNS_Real holds f . x = <*x*> ) ) by A2, A10, A14, NORMSP_3:def 11; :: thesis: verum