set T = TPlane (p,(0. ()));
defpred S1[ object , object ] means for q being Point of () 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. ()))) & S1[x,y] )
proof
let x be object ; :: thesis: ( x in [#] S implies ex y being object st
( y in [#] (TPlane (p,(0. ()))) & S1[x,y] ) )

assume A3: x in [#] S ; :: thesis: ex y being object st
( y in [#] (TPlane (p,(0. ()))) & S1[x,y] )

[#] S c= [#] () by PRE_TOPC:def 4;
then reconsider q = x as Point of () 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. ()))) & S1[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 ;
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. ())))| = 0 by RLVECT_1:4;
then |(p,(((1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))) + ((- 1) * (0. ()))))| = 0 by RLVECT_1:10;
then |(p,(((1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))) - (0. ())))| = 0 by RLVECT_1:16;
then (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) in Plane (p,(0. ())) ;
hence (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) in [#] (TPlane (p,(0. ()))) by PRE_TOPC:def 5; :: thesis: S1[x,(1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))]
thus S1[x,(1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))] ; :: thesis: verum
end;
consider f being Function of ([#] S),([#] (TPlane (p,(0. ())))) such that
A6: for x being object st x in [#] S holds
S1[x,f . x] from reconsider f = f as Function of S,(TPlane (p,(0. ()))) ;
take f ; :: thesis: for q being Point of () st q in S holds
f . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))

let q be Point of (); :: 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