defpred S_{1}[ object , object ] means ex q being Point of (TOP-REAL n) st

( q = $1 & $2 = |(p,q)| );

A1: for x being object st x in the carrier of (TOP-REAL n) holds

ex y being object st S_{1}[x,y]

A2: ( dom f1 = the carrier of (TOP-REAL n) & ( for x being object st x in the carrier of (TOP-REAL n) holds

S_{1}[x,f1 . x] ) )
from CLASSES1:sch 1(A1);

rng f1 c= the carrier of R^1

take f2 ; :: thesis: for q being Point of (TOP-REAL n) holds f2 . q = |(p,q)|

for q being Point of (TOP-REAL n) holds f1 . q = |(p,q)|

( q = $1 & $2 = |(p,q)| );

A1: for x being object st x in the carrier of (TOP-REAL n) holds

ex y being object st S

proof

consider f1 being Function such that
let x be object ; :: thesis: ( x in the carrier of (TOP-REAL n) implies ex y being object st S_{1}[x,y] )

assume x in the carrier of (TOP-REAL n) ; :: thesis: ex y being object st S_{1}[x,y]

then reconsider q3 = x as Point of (TOP-REAL n) ;

take |(p,q3)| ; :: thesis: S_{1}[x,|(p,q3)|]

thus S_{1}[x,|(p,q3)|]
; :: thesis: verum

end;assume x in the carrier of (TOP-REAL n) ; :: thesis: ex y being object st S

then reconsider q3 = x as Point of (TOP-REAL n) ;

take |(p,q3)| ; :: thesis: S

thus S

A2: ( dom f1 = the carrier of (TOP-REAL n) & ( for x being object st x in the carrier of (TOP-REAL n) holds

S

rng f1 c= the carrier of R^1

proof

then reconsider f2 = f1 as Function of (TOP-REAL n),R^1 by A2, FUNCT_2:def 1, RELSET_1:4;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng f1 or z in the carrier of R^1 )

assume z in rng f1 ; :: thesis: z in the carrier of R^1

then consider xz being object such that

A3: xz in dom f1 and

A4: z = f1 . xz by FUNCT_1:def 3;

ex q4 being Point of (TOP-REAL n) st

( q4 = xz & f1 . xz = |(p,q4)| ) by A2, A3;

hence z in the carrier of R^1 by A4, TOPMETR:17, XREAL_0:def 1; :: thesis: verum

end;assume z in rng f1 ; :: thesis: z in the carrier of R^1

then consider xz being object such that

A3: xz in dom f1 and

A4: z = f1 . xz by FUNCT_1:def 3;

ex q4 being Point of (TOP-REAL n) st

( q4 = xz & f1 . xz = |(p,q4)| ) by A2, A3;

hence z in the carrier of R^1 by A4, TOPMETR:17, XREAL_0:def 1; :: thesis: verum

take f2 ; :: thesis: for q being Point of (TOP-REAL n) holds f2 . q = |(p,q)|

for q being Point of (TOP-REAL n) holds f1 . q = |(p,q)|

proof

hence
for q being Point of (TOP-REAL n) holds f2 . q = |(p,q)|
; :: thesis: verum
let q be Point of (TOP-REAL n); :: thesis: f1 . q = |(p,q)|

ex q2 being Point of (TOP-REAL n) st

( q2 = q & f1 . q = |(p,q2)| ) by A2;

hence f1 . q = |(p,q)| ; :: thesis: verum

end;ex q2 being Point of (TOP-REAL n) st

( q2 = q & f1 . q = |(p,q2)| ) by A2;

hence f1 . q = |(p,q)| ; :: thesis: verum