begin
Lm1:
for n being Nat holds the carrier of (RealVectSpace (Seg n)) = the carrier of (TOP-REAL n)
Lm2:
for n being Nat holds 0. (RealVectSpace (Seg n)) = 0. (TOP-REAL n)
begin
Lm3:
for n being Nat
for p0 being Point of (TOP-REAL (n + 1)) st p0 = Base_FinSeq ((n + 1),(n + 1)) holds
TOP-REAL n, TPlane (p0,(0. (TOP-REAL (n + 1)))) are_homeomorphic
begin
definition
let n be
Nat;
let p be
Point of
(TOP-REAL n);
let S be
SubSpace of
TOP-REAL n;
assume A1:
p in Sphere (
(0. (TOP-REAL n)),1)
;
existence
ex b1 being Function of S,(TPlane (p,(0. (TOP-REAL n)))) st
for q being Point of (TOP-REAL n) st q in S holds
b1 . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))
uniqueness
for b1, b2 being Function of S,(TPlane (p,(0. (TOP-REAL n)))) st ( for q being Point of (TOP-REAL n) st q in S holds
b1 . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) ) & ( for q being Point of (TOP-REAL n) st q in S holds
b2 . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) ) holds
b1 = b2
end;