set T = TPlane (p,(0. (TOP-REAL n)));
defpred S₁[ 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₁[x,y] )

proof

let x be object ; :: thesis: ( x in [#] S implies ex y being object st
( y in [#] (TPlane (p,(0. (TOP-REAL n)))) & S₁[x,y] ) )
assume A3: x in [#] S ; :: thesis: ex y being object st
( y in [#] (TPlane (p,(0. (TOP-REAL n)))) & S₁[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₁[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₁[x,(1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))]
thus S₁[x,(1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))] ; :: thesis: verum

end;

consider f being Function of ([#] S),([#] (TPlane (p,(0. (TOP-REAL n))))) such that
A6: for x being object st x in [#] S holds
S₁[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