environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, ORDINAL1, PRE_TOPC, EUCLID, ARYTM_1, ARYTM_3, SUPINF_2, XBOOLE_0, PRVECT_1, FUNCOP_1, XXREAL_0, RLSUB_2, ORDINAL2, METRIC_1, TARSKI, STRUCT_0, REAL_1, MATRIXR2, FINSEQ_1, FINSEQ_2, COMPTS_1, BINOP_2, TOPS_2, T_0TOPSP, CONNSP_2, FUNCT_1, RELAT_1, CARD_1, FUNCT_2, VALUED_1, WAYBEL23, RLVECT_3, FINSET_1, NAT_1, PARTFUN1, SETFAM_1, ORDINAL4, ALGSTR_0, EUCLID_7, CARD_3, RCOMP_1, TOPREALB, RVSUM_1, RLSUB_1, RLVECT_2, FUNCSDOM, RLVECT_1, RLTOPSP1, VECTSP_1, MATRIX_1, MATRLIN2, RLVECT_5, ZFMISC_1, PCOMPS_1, COMPLEX1, SQUARE_1, TOPMETR, INCSP_1, MFOLD_1, MFOLD_2;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, FUNCOP_1, FUNCT_1, TOPS_2, RELAT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, ORDINAL1, NUMBERS, XREAL_0, XXREAL_0, COMPLEX1, REAL_1, NAT_1, RVSUM_1, PRE_TOPC, METRIC_1, TOPREAL9, CONNSP_2, METRIZTS, COMPTS_1, EUCLID, SQUARE_1, TOPMETR, TMAP_1, WAYBEL23, CARD_1, TOPREALB, RLSUB_1, RLVECT_3, RLTOPSP1, PRVECT_1, VECTSP_1, MATRIX_1, MATRIX_6, MATRTOP1, RLVECT_2, RLVECT_5, FUNCSDOM, FINSEQ_1, FINSET_1, FINSEQ_2, EUCLID_7, STRUCT_0, RLVECT_1, RLSUB_2, T_0TOPSP, XCMPLX_0, BINOP_2, ZFMISC_1, NAT_D, PCOMPS_1, MFOLD_1;
definitions TARSKI, FUNCT_1;
theorems TOPREAL9, TOPREALB, METRIZTS, TSEP_1, YELLOW14, T_0TOPSP, RLVECT_5, ZFMISC_1, TARSKI, RELAT_1, FUNCT_1, RLTOPSP1, EUCLID, FUNCT_2, RLSUB_1, XBOOLE_0, EUCLID_2, JGRAPH_5, ORDINAL1, RLVECT_3, MATRTOP2, FUNCSDOM, FINSEQ_2, EUCLID_7, CARD_1, RLVECT_2, RLVECT_1, NAT_1, PARTFUN1, FINSEQ_3, MATRIX13, FINSEQ_1, RLSUB_2, RLVECT_4, XCMPLX_1, PRE_TOPC, WAYBEL23, TOPS_2, BORSUK_3, CONNSP_2, XBOOLE_1, TSP_1, SUBSET_1, RVSUM_1, FUNCOP_1, VALUED_1, MATRIXR2, RELSET_1, XREAL_1, FINSEQ_4, PCOMPS_1, XREAL_0, JORDAN, REAL_NS1, SQUARE_1, XXREAL_0, METRIC_1, TOPMETR, TOPREAL3, UNIFORM1, JGRAPH_1, JGRAPH_2, JGRAPH_6, TMAP_1, JORDAN2C, FRECHET, MFOLD_1, FUNCTOR0, RLAFFIN3, XTUPLE_0;
schemes NAT_1, FUNCT_2, CLASSES1;
registrations XBOOLE_0, XXREAL_0, XREAL_0, XCMPLX_0, SQUARE_1, NAT_1, STRUCT_0, METRIC_1, MONOID_0, EUCLID, VALUED_0, FINSEQ_1, FUNCT_1, RELAT_1, PRE_TOPC, TOPS_1, TOPREAL9, TMAP_1, COMPTS_1, TOPMETR, METRIZTS, RLVECT_3, TOPREAL1, SUBSET_1, TOPREALB, VECTSP_1, EUCLID_7, FINSET_1, FUNCT_2, FINSEQ_2, RLSUB_1, ORDINAL1, MATRTOP1, RVSUM_1, NUMBERS, RLTOPSP1, RELSET_1, MFOLD_1, RLAFFIN3;
constructors HIDDEN, MONOID_0, TOPREAL9, TOPREALB, SQUARE_1, FUNCSDOM, METRIZTS, PCOMPS_1, COMPTS_1, BINOP_2, TMAP_1, WAYBEL23, RLVECT_3, PRVECT_1, MATRIX_6, MATRTOP1, RLVECT_5, EUCLID_7, FVSUM_1, RLSUB_2, BORSUK_3, NAT_D, CONVEX1, MFOLD_1, REAL_1;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
equalities EUCLID, FINSEQ_1, STRUCT_0, VECTSP_1, RLVECT_1;
expansions FINSEQ_1, STRUCT_0, TARSKI, FUNCT_1;
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)
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
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;