defpred S1[ object , object ] means for p being Point of (TOP-REAL 2) st p = $1 holds
$2 = tricord3 (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 ;
( 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)
;
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) ;
A2:
tricord3 (
p1,
p2,
p3,
p0)
in REAL
by XREAL_0:def 1;
S1[
x,
tricord3 (
p1,
p2,
p3,
p0)]
;
hence
ex
y being
object st
(
y in the
carrier of
R^1 &
S1[
x,
y] )
by A2, TOPMETR:17;
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
A3:
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 = tricord3 (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 = tricord3 (p1,p2,p3,p)
by A3;
hence
ex b1 being Function of (TOP-REAL 2),R^1 st
for p being Point of (TOP-REAL 2) holds b1 . p = tricord3 (p1,p2,p3,p)
; verum