set T = TPlane (p,(0. (TOP-REAL n)));
defpred S1[ 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)))) & S1[x,y] )
proof
let x be
object ;
( x in [#] S implies ex y being object st
( y in [#] (TPlane (p,(0. (TOP-REAL n)))) & S1[x,y] ) )
assume A3:
x in [#] S
;
ex y being object st
( y in [#] (TPlane (p,(0. (TOP-REAL n)))) & S1[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))
;
( (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) in [#] (TPlane (p,(0. (TOP-REAL n)))) & 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 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;
S1[x,(1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))]
thus
S1[
x,
(1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))]
;
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
S1[x,f . x]
from FUNCT_2:sch 1(A2);
reconsider f = f as Function of S,(TPlane (p,(0. (TOP-REAL n)))) ;
take
f
; 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); ( q in S implies f . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) )
assume A7:
q in S
; f . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))
thus
f . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))
by A6, A7; verum