defpred S_{1}[ object , object ] means for p being Point of (TOP-REAL 2) st p = $1 holds

$2 = tricord2 (p1,p2,p3,p);

set X = the carrier of (TOP-REAL 2);

set Y = the carrier of R^1;

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

ex y being object st

( y in the carrier of R^1 & S_{1}[x,y] )

for x being object st x in the carrier of (TOP-REAL 2) holds

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

then consider g being Function of the carrier of (TOP-REAL 2), the carrier of R^1 such that

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

for p being Point of (TOP-REAL 2) st p = x holds

g . x = tricord2 (p1,p2,p3,p) ;

reconsider f0 = g as Function of (TOP-REAL 2),R^1 ;

for p being Point of (TOP-REAL 2) holds f0 . p = tricord2 (p1,p2,p3,p) by A2;

hence ex b_{1} being Function of (TOP-REAL 2),R^1 st

for p being Point of (TOP-REAL 2) holds b_{1} . p = tricord2 (p1,p2,p3,p)
; :: thesis: verum

$2 = tricord2 (p1,p2,p3,p);

set X = the carrier of (TOP-REAL 2);

set Y = the carrier of R^1;

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

ex y being object st

( y in the carrier of R^1 & S

proof

ex f being Function of the carrier of (TOP-REAL 2), the carrier of R^1 st
let x be object ; :: thesis: ( x in the carrier of (TOP-REAL 2) implies ex y being object st

( y in the carrier of R^1 & S_{1}[x,y] ) )

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

( y in the carrier of R^1 & S_{1}[x,y] )

then reconsider p0 = x as Point of (TOP-REAL 2) ;

reconsider t = tricord2 (p1,p2,p3,p0) as Element of REAL by XREAL_0:def 1;

S_{1}[x,t]
;

hence ex y being object st

( y in the carrier of R^1 & S_{1}[x,y] )
by TOPMETR:17; :: thesis: verum

end;( y in the carrier of R^1 & S

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

( y in the carrier of R^1 & S

then reconsider p0 = x as Point of (TOP-REAL 2) ;

reconsider t = tricord2 (p1,p2,p3,p0) as Element of REAL by XREAL_0:def 1;

S

hence ex y being object st

( y in the carrier of R^1 & S

for x being object st x in the carrier of (TOP-REAL 2) holds

S

then consider g being Function of the carrier of (TOP-REAL 2), the carrier of R^1 such that

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

for p being Point of (TOP-REAL 2) st p = x holds

g . x = tricord2 (p1,p2,p3,p) ;

reconsider f0 = g as Function of (TOP-REAL 2),R^1 ;

for p being Point of (TOP-REAL 2) holds f0 . p = tricord2 (p1,p2,p3,p) by A2;

hence ex b

for p being Point of (TOP-REAL 2) holds b