defpred S1[ 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 & S1[x,y] )
proof
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 & S1[x,y] ) )
assume x in the carrier of (TOP-REAL 2) ; :: thesis: ex y being object st
( y in the carrier of R^1 & S1[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;
S1[x,t] ;
hence ex y being object st
( y in the carrier of R^1 & S1[x,y] ) by TOPMETR:17; :: thesis: verum
end;
ex f being Function of the carrier of (TOP-REAL 2), the carrier of R^1 st
for x being object st x in the carrier of (TOP-REAL 2) holds
S1[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 b1 being Function of (TOP-REAL 2),R^1 st
for p being Point of (TOP-REAL 2) holds b1 . p = tricord2 (p1,p2,p3,p) ; :: thesis: verum