set T = TPlane (p,(0. (TOP-REAL n)));

defpred S_{1}[ object , object ] means for q being Point of (TOP-REAL n) st q = $1 & q in S holds

$2 = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p));

A2: for x being object st x in [#] S holds

ex y being object st

( y in [#] (TPlane (p,(0. (TOP-REAL n)))) & S_{1}[x,y] )

A6: for x being object st x in [#] S holds

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

reconsider f = f as Function of S,(TPlane (p,(0. (TOP-REAL n)))) ;

take f ; :: thesis: for q being Point of (TOP-REAL n) st q in S holds

f . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))

let q be Point of (TOP-REAL n); :: thesis: ( q in S implies f . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) )

assume A7: q in S ; :: thesis: f . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))

thus f . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) by A6, A7; :: thesis: verum

defpred S

$2 = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p));

A2: for x being object st x in [#] S holds

ex y being object st

( y in [#] (TPlane (p,(0. (TOP-REAL n)))) & S

proof

consider f being Function of ([#] S),([#] (TPlane (p,(0. (TOP-REAL n))))) such that
let x be object ; :: thesis: ( x in [#] S implies ex y being object st

( y in [#] (TPlane (p,(0. (TOP-REAL n)))) & S_{1}[x,y] ) )

assume A3: x in [#] S ; :: thesis: ex y being object st

( y in [#] (TPlane (p,(0. (TOP-REAL n)))) & S_{1}[x,y] )

[#] S c= [#] (TOP-REAL n) by PRE_TOPC:def 4;

then reconsider q = x as Point of (TOP-REAL n) by A3;

set y = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p));

take (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) ; :: thesis: ( (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) in [#] (TPlane (p,(0. (TOP-REAL n)))) & S_{1}[x,(1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))] )

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

reconsider p1 = p as Point of (TOP-REAL n1) ;

|.(p1 - (0. (TOP-REAL n1))).| = 1 by A1, TOPREAL9:9;

then |.(p1 + ((- 1) * (0. (TOP-REAL n1)))).| = 1 by RLVECT_1:16;

then |.(p1 + (0. (TOP-REAL n1))).| = 1 by RLVECT_1:10;

then |.p.| = 1 by RLVECT_1:4;

then |(p,p)| = 1 ^2 by EUCLID_2:4;

then A4: |(p,p)| = 1 * 1 by SQUARE_1:def 1;

A5: |(p,(|(q,p)| * p))| = |(q,p)| * |(p,p)| by EUCLID_2:20

.= |(p,q)| by A4 ;

|(p,((1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))))| = (1 / (1 - |(q,p)|)) * |(p,(q - (|(q,p)| * p)))| by EUCLID_2:20

.= (1 / (1 - |(q,p)|)) * (|(p,q)| - |(p,(|(q,p)| * p))|) by EUCLID_2:27

.= 0 by A5 ;

then |(p,(((1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))) + (0. (TOP-REAL n))))| = 0 by RLVECT_1:4;

then |(p,(((1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))) + ((- 1) * (0. (TOP-REAL n)))))| = 0 by RLVECT_1:10;

then |(p,(((1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))) - (0. (TOP-REAL n))))| = 0 by RLVECT_1:16;

then (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) in Plane (p,(0. (TOP-REAL n))) ;

hence (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) in [#] (TPlane (p,(0. (TOP-REAL n)))) by PRE_TOPC:def 5; :: thesis: S_{1}[x,(1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))]

thus S_{1}[x,(1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))]
; :: thesis: verum

end;( y in [#] (TPlane (p,(0. (TOP-REAL n)))) & S

assume A3: x in [#] S ; :: thesis: ex y being object st

( y in [#] (TPlane (p,(0. (TOP-REAL n)))) & S

[#] S c= [#] (TOP-REAL n) by PRE_TOPC:def 4;

then reconsider q = x as Point of (TOP-REAL n) by A3;

set y = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p));

take (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) ; :: thesis: ( (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) in [#] (TPlane (p,(0. (TOP-REAL n)))) & S

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

reconsider p1 = p as Point of (TOP-REAL n1) ;

|.(p1 - (0. (TOP-REAL n1))).| = 1 by A1, TOPREAL9:9;

then |.(p1 + ((- 1) * (0. (TOP-REAL n1)))).| = 1 by RLVECT_1:16;

then |.(p1 + (0. (TOP-REAL n1))).| = 1 by RLVECT_1:10;

then |.p.| = 1 by RLVECT_1:4;

then |(p,p)| = 1 ^2 by EUCLID_2:4;

then A4: |(p,p)| = 1 * 1 by SQUARE_1:def 1;

A5: |(p,(|(q,p)| * p))| = |(q,p)| * |(p,p)| by EUCLID_2:20

.= |(p,q)| by A4 ;

|(p,((1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))))| = (1 / (1 - |(q,p)|)) * |(p,(q - (|(q,p)| * p)))| by EUCLID_2:20

.= (1 / (1 - |(q,p)|)) * (|(p,q)| - |(p,(|(q,p)| * p))|) by EUCLID_2:27

.= 0 by A5 ;

then |(p,(((1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))) + (0. (TOP-REAL n))))| = 0 by RLVECT_1:4;

then |(p,(((1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))) + ((- 1) * (0. (TOP-REAL n)))))| = 0 by RLVECT_1:10;

then |(p,(((1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))) - (0. (TOP-REAL n))))| = 0 by RLVECT_1:16;

then (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) in Plane (p,(0. (TOP-REAL n))) ;

hence (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) in [#] (TPlane (p,(0. (TOP-REAL n)))) by PRE_TOPC:def 5; :: thesis: S

thus S

A6: for x being object st x in [#] S holds

S

reconsider f = f as Function of S,(TPlane (p,(0. (TOP-REAL n)))) ;

take f ; :: thesis: for q being Point of (TOP-REAL n) st q in S holds

f . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))

let q be Point of (TOP-REAL n); :: thesis: ( q in S implies f . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) )

assume A7: q in S ; :: thesis: f . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))

thus f . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) by A6, A7; :: thesis: verum