:: MFOLD_2 semantic presentation begin registration cluster {} -> {} -valued ; correctness coherence {} is {} -valued ; by FUNCTOR0:1; cluster {} -> onto ; correctness coherence {} is onto ; proof rng {} = {} ; hence {} is onto by FUNCT_2:def_3; ::_thesis: verum end; end; theorem Th1: :: MFOLD_2:1 for f being Function for Y being set holds dom (Y |` f) = f " Y proof let f be Function; ::_thesis: for Y being set holds dom (Y |` f) = f " Y let Y be set ; ::_thesis: dom (Y |` f) = f " Y for x being set holds ( x in dom (Y |` f) iff x in f " Y ) proof let x be set ; ::_thesis: ( x in dom (Y |` f) iff x in f " Y ) hereby ::_thesis: ( x in f " Y implies x in dom (Y |` f) ) assume x in dom (Y |` f) ; ::_thesis: x in f " Y then consider y being set such that A1: [x,y] in Y |` f by XTUPLE_0:def_12; ( y in Y & [x,y] in f ) by A1, RELAT_1:def_12; hence x in f " Y by RELAT_1:def_14; ::_thesis: verum end; assume x in f " Y ; ::_thesis: x in dom (Y |` f) then consider y being set such that A2: ( [x,y] in f & y in Y ) by RELAT_1:def_14; [x,y] in Y |` f by A2, RELAT_1:def_12; hence x in dom (Y |` f) by XTUPLE_0:def_12; ::_thesis: verum end; hence dom (Y |` f) = f " Y by TARSKI:1; ::_thesis: verum end; theorem Th2: :: MFOLD_2:2 for f being Function for Y1, Y2 being set st Y2 c= Y1 holds (Y1 |` f) " Y2 = f " Y2 proof let f be Function; ::_thesis: for Y1, Y2 being set st Y2 c= Y1 holds (Y1 |` f) " Y2 = f " Y2 let Y1, Y2 be set ; ::_thesis: ( Y2 c= Y1 implies (Y1 |` f) " Y2 = f " Y2 ) assume A1: Y2 c= Y1 ; ::_thesis: (Y1 |` f) " Y2 = f " Y2 for x being set holds ( x in (Y1 |` f) " Y2 iff x in f " Y2 ) proof let x be set ; ::_thesis: ( x in (Y1 |` f) " Y2 iff x in f " Y2 ) hereby ::_thesis: ( x in f " Y2 implies x in (Y1 |` f) " Y2 ) assume x in (Y1 |` f) " Y2 ; ::_thesis: x in f " Y2 then consider y being set such that A2: ( [x,y] in Y1 |` f & y in Y2 ) by RELAT_1:def_14; [x,y] in f by A2, RELAT_1:def_12; hence x in f " Y2 by A2, RELAT_1:def_14; ::_thesis: verum end; assume x in f " Y2 ; ::_thesis: x in (Y1 |` f) " Y2 then consider y being set such that A3: ( [x,y] in f & y in Y2 ) by RELAT_1:def_14; [x,y] in Y1 |` f by A3, A1, RELAT_1:def_12; hence x in (Y1 |` f) " Y2 by A3, RELAT_1:def_14; ::_thesis: verum end; hence (Y1 |` f) " Y2 = f " Y2 by TARSKI:1; ::_thesis: verum end; theorem Th3: :: MFOLD_2:3 for S, T being TopStruct for f being Function of S,T st f is being_homeomorphism holds f " is being_homeomorphism proof let S, T be TopStruct ; ::_thesis: for f being Function of S,T st f is being_homeomorphism holds f " is being_homeomorphism let f be Function of S,T; ::_thesis: ( f is being_homeomorphism implies f " is being_homeomorphism ) assume A1: f is being_homeomorphism ; ::_thesis: f " is being_homeomorphism then A2: ( dom f = [#] S & rng f = [#] T & f is one-to-one & f is continuous & f " is continuous ) by TOPS_2:def_5; percases ( ( not S is empty & not T is empty ) or S is empty or T is empty ) ; suppose ( not S is empty & not T is empty ) ; ::_thesis: f " is being_homeomorphism hence f " is being_homeomorphism by A1, TOPS_2:56; ::_thesis: verum end; supposeA3: ( S is empty or T is empty ) ; ::_thesis: f " is being_homeomorphism A4: f = {} proof percases ( S is empty or T is empty ) by A3; suppose S is empty ; ::_thesis: f = {} hence f = {} ; ::_thesis: verum end; suppose T is empty ; ::_thesis: f = {} hence f = {} ; ::_thesis: verum end; end; end; reconsider g = f as one-to-one onto PartFunc of {},{} by A4, FUNCTOR0:1; A5: f " = g " by A2; A6: ( dom (f ") = [#] T & rng (f ") = [#] S ) by A2, A4; reconsider g1 = f " as one-to-one onto PartFunc of {},{} by A5; (f ") " = g1 " by A2, A4; hence f " is being_homeomorphism by A4, A6, A2, TOPS_2:def_5; ::_thesis: verum end; end; end; definition let S, T be TopStruct ; :: original: are_homeomorphic redefine predS,T are_homeomorphic ; symmetry for S, T being TopStruct st R91(b1,b2) holds R91(b2,b1) proof let S, T be TopStruct ; ::_thesis: ( R91(S,T) implies R91(T,S) ) assume S,T are_homeomorphic ; ::_thesis: R91(T,S) then consider f being Function of S,T such that A1: f is being_homeomorphism by T_0TOPSP:def_1; f " is being_homeomorphism by A1, Th3; hence R91(T,S) by T_0TOPSP:def_1; ::_thesis: verum end; end; theorem Th4: :: MFOLD_2:4 for T1, T2 being TopSpace for A2 being Subset of T2 for f being Function of T1,T2 st f is being_homeomorphism holds for g being Function of (T1 | (f " A2)),(T2 | A2) st g = A2 |` f holds g is being_homeomorphism proof let T1, T2 be TopSpace; ::_thesis: for A2 being Subset of T2 for f being Function of T1,T2 st f is being_homeomorphism holds for g being Function of (T1 | (f " A2)),(T2 | A2) st g = A2 |` f holds g is being_homeomorphism let A2 be Subset of T2; ::_thesis: for f being Function of T1,T2 st f is being_homeomorphism holds for g being Function of (T1 | (f " A2)),(T2 | A2) st g = A2 |` f holds g is being_homeomorphism let f be Function of T1,T2; ::_thesis: ( f is being_homeomorphism implies for g being Function of (T1 | (f " A2)),(T2 | A2) st g = A2 |` f holds g is being_homeomorphism ) assume A1: f is being_homeomorphism ; ::_thesis: for g being Function of (T1 | (f " A2)),(T2 | A2) st g = A2 |` f holds g is being_homeomorphism A2: ( dom f = [#] T1 & rng f = [#] T2 ) by A1, TOPS_2:def_5; T1,T2 are_homeomorphic by A1, T_0TOPSP:def_1; then ( T1 is empty iff T2 is empty ) by YELLOW14:18; then A3: ( [#] T1 = {} iff [#] T2 = {} ) ; A4: rng f = [#] T2 by A1, TOPS_2:def_5; set A = f " A2; let g be Function of (T1 | (f " A2)),(T2 | A2); ::_thesis: ( g = A2 |` f implies g is being_homeomorphism ) assume A5: g = A2 |` f ; ::_thesis: g is being_homeomorphism A6: rng g = A2 by A2, A5, RELAT_1:89; A7: f is one-to-one by A1, TOPS_2:def_5; then A8: g is one-to-one by A5, FUNCT_1:58; A9: dom g = f " A2 by A5, Th1; set TA = T1 | (f " A2); set TB = T2 | A2; A10: [#] (T1 | (f " A2)) = f " A2 by PRE_TOPC:def_5; A11: ( [#] (T1 | (f " A2)) = {} iff [#] (T2 | A2) = {} ) by A6; A12: [#] (T2 | A2) = A2 by PRE_TOPC:def_5; A13: f is continuous by A1, TOPS_2:def_5; for P being Subset of (T2 | A2) st P is open holds g " P is open proof let P be Subset of (T2 | A2); ::_thesis: ( P is open implies g " P is open ) assume P is open ; ::_thesis: g " P is open then consider P1 being Subset of T2 such that A14: P1 is open and A15: P = P1 /\ A2 by A12, TSP_1:def_1; A16: f " P1 is open by A3, A13, A14, TOPS_2:43; g " P = f " P by A5, Th2, A15, XBOOLE_1:17 .= (f " P1) /\ the carrier of (T1 | (f " A2)) by A10, A15, FUNCT_1:68 ; hence g " P is open by A16, TSP_1:def_1; ::_thesis: verum end; then A17: g is continuous by A11, TOPS_2:43; A18: f " is continuous by A1, TOPS_2:def_5; for P being Subset of (T1 | (f " A2)) st P is open holds (g ") " P is open proof let P be Subset of (T1 | (f " A2)); ::_thesis: ( P is open implies (g ") " P is open ) assume P is open ; ::_thesis: (g ") " P is open then consider P1 being Subset of T1 such that A19: P1 is open and A20: P = P1 /\ (f " A2) by A10, TSP_1:def_1; A21: (f ") " P1 is open by A3, A18, A19, TOPS_2:43; A2 = f .: (f " A2) by A2, FUNCT_1:77; then A22: the carrier of (T2 | A2) = (f ") " (f " A2) by A12, A4, A7, TOPS_2:54; (g ") " P = (A2 |` f) .: P by A5, A6, A8, A12, TOPS_2:54 .= (f .: P) /\ the carrier of (T2 | A2) by A12, FUNCT_1:67 .= ((f ") " (P1 /\ (f " A2))) /\ the carrier of (T2 | A2) by A4, A7, A20, TOPS_2:54 .= (((f ") " P1) /\ ((f ") " (f " A2))) /\ the carrier of (T2 | A2) by FUNCT_1:68 .= ((f ") " P1) /\ (((f ") " (f " A2)) /\ the carrier of (T2 | A2)) by XBOOLE_1:16 .= ((f ") " P1) /\ the carrier of (T2 | A2) by A22 ; hence (g ") " P is open by A21, TSP_1:def_1; ::_thesis: verum end; then g " is continuous by A11, TOPS_2:43; hence g is being_homeomorphism by A6, A9, A10, A8, A12, A17, TOPS_2:def_5; ::_thesis: verum end; theorem Th5: :: MFOLD_2:5 for T1, T2 being TopSpace for A2 being Subset of T2 for f being Function of T1,T2 st f is being_homeomorphism holds f " A2,A2 are_homeomorphic proof let T1, T2 be TopSpace; ::_thesis: for A2 being Subset of T2 for f being Function of T1,T2 st f is being_homeomorphism holds f " A2,A2 are_homeomorphic let A2 be Subset of T2; ::_thesis: for f being Function of T1,T2 st f is being_homeomorphism holds f " A2,A2 are_homeomorphic let f be Function of T1,T2; ::_thesis: ( f is being_homeomorphism implies f " A2,A2 are_homeomorphic ) assume A1: f is being_homeomorphism ; ::_thesis: f " A2,A2 are_homeomorphic A2: dom (A2 |` f) = f " A2 by Th1 .= [#] (T1 | (f " A2)) by PRE_TOPC:def_5 ; rng f = [#] T2 by A1, TOPS_2:def_5; then rng (A2 |` f) = A2 by RELAT_1:89 .= [#] (T2 | A2) by PRE_TOPC:def_5 ; then reconsider g = A2 |` f as Function of (T1 | (f " A2)),(T2 | A2) by A2, FUNCT_2:1; g is being_homeomorphism by A1, Th4; then T1 | (f " A2),T2 | A2 are_homeomorphic by T_0TOPSP:def_1; hence f " A2,A2 are_homeomorphic by METRIZTS:def_1; ::_thesis: verum end; theorem :: MFOLD_2:6 for T1, T2 being TopSpace for A1 being Subset of T1 for A2 being Subset of T2 st A1,A2 are_homeomorphic holds A2,A1 are_homeomorphic proof let T1, T2 be TopSpace; ::_thesis: for A1 being Subset of T1 for A2 being Subset of T2 st A1,A2 are_homeomorphic holds A2,A1 are_homeomorphic let A1 be Subset of T1; ::_thesis: for A2 being Subset of T2 st A1,A2 are_homeomorphic holds A2,A1 are_homeomorphic let A2 be Subset of T2; ::_thesis: ( A1,A2 are_homeomorphic implies A2,A1 are_homeomorphic ) assume A1,A2 are_homeomorphic ; ::_thesis: A2,A1 are_homeomorphic then T1 | A1,T2 | A2 are_homeomorphic by METRIZTS:def_1; hence A2,A1 are_homeomorphic by METRIZTS:def_1; ::_thesis: verum end; theorem Th7: :: MFOLD_2:7 for T1, T2 being TopSpace for A1 being Subset of T1 for A2 being Subset of T2 st A1,A2 are_homeomorphic holds ( A1 is empty iff A2 is empty ) proof let T1, T2 be TopSpace; ::_thesis: for A1 being Subset of T1 for A2 being Subset of T2 st A1,A2 are_homeomorphic holds ( A1 is empty iff A2 is empty ) let A1 be Subset of T1; ::_thesis: for A2 being Subset of T2 st A1,A2 are_homeomorphic holds ( A1 is empty iff A2 is empty ) let A2 be Subset of T2; ::_thesis: ( A1,A2 are_homeomorphic implies ( A1 is empty iff A2 is empty ) ) assume A1,A2 are_homeomorphic ; ::_thesis: ( A1 is empty iff A2 is empty ) then T1 | A1,T2 | A2 are_homeomorphic by METRIZTS:def_1; then consider f being Function of (T1 | A1),(T2 | A2) such that A1: f is being_homeomorphism by T_0TOPSP:def_1; ( dom f = [#] (T1 | A1) & rng f = [#] (T2 | A2) & f is one-to-one & f is continuous & f " is continuous ) by A1, TOPS_2:def_5; hence ( A1 is empty iff A2 is empty ) by PRE_TOPC:def_5; ::_thesis: verum end; theorem Th8: :: MFOLD_2:8 for T1, T2, T3 being TopSpace for A1 being Subset of T1 for A2 being Subset of T2 for A3 being Subset of T3 st A1,A2 are_homeomorphic & A2,A3 are_homeomorphic holds A1,A3 are_homeomorphic proof let T1, T2, T3 be TopSpace; ::_thesis: for A1 being Subset of T1 for A2 being Subset of T2 for A3 being Subset of T3 st A1,A2 are_homeomorphic & A2,A3 are_homeomorphic holds A1,A3 are_homeomorphic let A1 be Subset of T1; ::_thesis: for A2 being Subset of T2 for A3 being Subset of T3 st A1,A2 are_homeomorphic & A2,A3 are_homeomorphic holds A1,A3 are_homeomorphic let A2 be Subset of T2; ::_thesis: for A3 being Subset of T3 st A1,A2 are_homeomorphic & A2,A3 are_homeomorphic holds A1,A3 are_homeomorphic let A3 be Subset of T3; ::_thesis: ( A1,A2 are_homeomorphic & A2,A3 are_homeomorphic implies A1,A3 are_homeomorphic ) assume A1: A1,A2 are_homeomorphic ; ::_thesis: ( not A2,A3 are_homeomorphic or A1,A3 are_homeomorphic ) then A2: T1 | A1,T2 | A2 are_homeomorphic by METRIZTS:def_1; assume A3: A2,A3 are_homeomorphic ; ::_thesis: A1,A3 are_homeomorphic then A4: T2 | A2,T3 | A3 are_homeomorphic by METRIZTS:def_1; percases ( not A2 is empty or A2 is empty ) ; supposeA5: not A2 is empty ; ::_thesis: A1,A3 are_homeomorphic then A6: ( not A1 is empty & not A3 is empty ) by A1, A3, Th7; ( not T1 is empty & not T2 is empty & not T3 is empty ) by A5, A1, A3, Th7; then T1 | A1,T3 | A3 are_homeomorphic by A2, A4, A6, A5, BORSUK_3:3; hence A1,A3 are_homeomorphic by METRIZTS:def_1; ::_thesis: verum end; suppose A2 is empty ; ::_thesis: A1,A3 are_homeomorphic then A7: ( A1 is empty & A3 is empty ) by A1, A3, Th7; reconsider f = {} as Function ; A8: ( the carrier of (T1 | A1) = {} & the carrier of (T3 | A3) = {} ) by A7; ( dom f = {} & rng f = {} ) ; then reconsider f = f as Function of (T1 | A1),(T3 | A3) by A8, FUNCT_2:1; A9: ( dom f = [#] (T1 | A1) & rng f = [#] (T3 | A3) ) by A8; for P1 being Subset of (T3 | A3) st P1 is closed holds f " P1 is closed ; then A10: f is continuous by PRE_TOPC:def_6; reconsider g = f as one-to-one onto PartFunc of {},{} by FUNCTOR0:1; for P1 being Subset of (T1 | A1) st P1 is closed holds (f ") " P1 is closed by A7; then f " is continuous by PRE_TOPC:def_6; then f is being_homeomorphism by A9, A10, TOPS_2:def_5; then T1 | A1,T3 | A3 are_homeomorphic by T_0TOPSP:def_1; hence A1,A3 are_homeomorphic by METRIZTS:def_1; ::_thesis: verum end; end; end; theorem Th9: :: MFOLD_2:9 for T1, T2 being TopSpace st T1 is second-countable & T1,T2 are_homeomorphic holds T2 is second-countable proof let T1, T2 be TopSpace; ::_thesis: ( T1 is second-countable & T1,T2 are_homeomorphic implies T2 is second-countable ) assume T1 is second-countable ; ::_thesis: ( not T1,T2 are_homeomorphic or T2 is second-countable ) then A1: weight T1 c= omega by WAYBEL23:def_6; assume T1,T2 are_homeomorphic ; ::_thesis: T2 is second-countable then weight T1 = weight T2 by METRIZTS:4; hence T2 is second-countable by A1, WAYBEL23:def_6; ::_thesis: verum end; theorem Th10: :: MFOLD_2:10 for M, N being non empty TopSpace st M is Hausdorff & M,N are_homeomorphic holds N is Hausdorff proof let M, N be non empty TopSpace; ::_thesis: ( M is Hausdorff & M,N are_homeomorphic implies N is Hausdorff ) assume A1: M is Hausdorff ; ::_thesis: ( not M,N are_homeomorphic or N is Hausdorff ) assume M,N are_homeomorphic ; ::_thesis: N is Hausdorff then consider f being Function of N,M such that A2: f is being_homeomorphism by T_0TOPSP:def_1; A3: ( dom f = [#] N & rng f = [#] M & f is one-to-one & f is continuous & f " is continuous ) by A2, TOPS_2:def_5; for p, q being Point of N st p <> q holds ex N1, N2 being Subset of N st ( N1 is open & N2 is open & p in N1 & q in N2 & N1 misses N2 ) proof let p, q be Point of N; ::_thesis: ( p <> q implies ex N1, N2 being Subset of N st ( N1 is open & N2 is open & p in N1 & q in N2 & N1 misses N2 ) ) assume p <> q ; ::_thesis: ex N1, N2 being Subset of N st ( N1 is open & N2 is open & p in N1 & q in N2 & N1 misses N2 ) then f . p <> f . q by A3, FUNCT_1:def_4; then consider M1, M2 being Subset of M such that A4: ( M1 is open & M2 is open & f . p in M1 & f . q in M2 & M1 misses M2 ) by A1, PRE_TOPC:def_10; reconsider N1 = f " M1 as Subset of N ; reconsider N2 = f " M2 as Subset of N ; take N1 ; ::_thesis: ex N2 being Subset of N st ( N1 is open & N2 is open & p in N1 & q in N2 & N1 misses N2 ) take N2 ; ::_thesis: ( N1 is open & N2 is open & p in N1 & q in N2 & N1 misses N2 ) thus ( N1 is open & N2 is open ) by A4, A3, TOPS_2:43; ::_thesis: ( p in N1 & q in N2 & N1 misses N2 ) thus ( p in N1 & q in N2 ) by A4, FUNCT_2:38; ::_thesis: N1 misses N2 thus N1 misses N2 by A4, FUNCT_1:71; ::_thesis: verum end; hence N is Hausdorff by PRE_TOPC:def_10; ::_thesis: verum end; theorem Th11: :: MFOLD_2:11 for n being Nat for M, N being non empty TopSpace st M is n -locally_euclidean & M,N are_homeomorphic holds N is n -locally_euclidean proof let n be Nat; ::_thesis: for M, N being non empty TopSpace st M is n -locally_euclidean & M,N are_homeomorphic holds N is n -locally_euclidean let M, N be non empty TopSpace; ::_thesis: ( M is n -locally_euclidean & M,N are_homeomorphic implies N is n -locally_euclidean ) assume A1: M is n -locally_euclidean ; ::_thesis: ( not M,N are_homeomorphic or N is n -locally_euclidean ) assume M,N are_homeomorphic ; ::_thesis: N is n -locally_euclidean then consider f being Function of N,M such that A2: f is being_homeomorphism by T_0TOPSP:def_1; A3: ( dom f = [#] N & rng f = [#] M & f is one-to-one & f is continuous & f " is continuous ) by A2, TOPS_2:def_5; for q being Point of N ex U being a_neighborhood of q ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic proof let q be Point of N; ::_thesis: ex U being a_neighborhood of q ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic set p = f . q; consider U1 being a_neighborhood of f . q, S1 being open Subset of (TOP-REAL n) such that A4: U1,S1 are_homeomorphic by A1, MFOLD_1:def_4; consider U2 being open Subset of M, S being open Subset of (TOP-REAL n) such that A5: ( U2 c= U1 & f . q in U2 & U2,S are_homeomorphic ) by A4, MFOLD_1:11; A6: f " U2 is open by A3, TOPS_2:43; q in f " U2 by A5, FUNCT_2:38; then reconsider U = f " U2 as a_neighborhood of q by A6, CONNSP_2:6; take U ; ::_thesis: ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic take S ; ::_thesis: U,S are_homeomorphic U,U2 are_homeomorphic by A2, Th5; hence U,S are_homeomorphic by A5, Th8; ::_thesis: verum end; hence N is n -locally_euclidean by MFOLD_1:def_4; ::_thesis: verum end; theorem Th12: :: MFOLD_2:12 for n being Nat for M, N being non empty TopSpace st M is n -manifold & M,N are_homeomorphic holds N is n -manifold proof let n be Nat; ::_thesis: for M, N being non empty TopSpace st M is n -manifold & M,N are_homeomorphic holds N is n -manifold let M, N be non empty TopSpace; ::_thesis: ( M is n -manifold & M,N are_homeomorphic implies N is n -manifold ) assume A1: M is n -manifold ; ::_thesis: ( not M,N are_homeomorphic or N is n -manifold ) assume A2: M,N are_homeomorphic ; ::_thesis: N is n -manifold then A3: N is second-countable by A1, Th9; A4: N is Hausdorff by A1, A2, Th10; N is n -locally_euclidean by A1, A2, Th11; hence N is n -manifold by A3, A4; ::_thesis: verum end; theorem Th13: :: MFOLD_2:13 for x1, x2 being FinSequence of REAL for i being Element of NAT st i in dom (mlt (x1,x2)) holds ( (mlt (x1,x2)) . i = (x1 /. i) * (x2 /. i) & (mlt (x1,x2)) /. i = (x1 /. i) * (x2 /. i) ) proof let x1, x2 be FinSequence of REAL ; ::_thesis: for i being Element of NAT st i in dom (mlt (x1,x2)) holds ( (mlt (x1,x2)) . i = (x1 /. i) * (x2 /. i) & (mlt (x1,x2)) /. i = (x1 /. i) * (x2 /. i) ) let i be Element of NAT ; ::_thesis: ( i in dom (mlt (x1,x2)) implies ( (mlt (x1,x2)) . i = (x1 /. i) * (x2 /. i) & (mlt (x1,x2)) /. i = (x1 /. i) * (x2 /. i) ) ) assume A1: i in dom (mlt (x1,x2)) ; ::_thesis: ( (mlt (x1,x2)) . i = (x1 /. i) * (x2 /. i) & (mlt (x1,x2)) /. i = (x1 /. i) * (x2 /. i) ) A2: mlt (x1,x2) = multreal .: (x1,x2) by RVSUM_1:def_9; ( dom multreal = [:REAL,REAL:] & rng x1 c= REAL ) by FUNCT_2:def_1; then [:(rng x1),(rng x2):] c= dom multreal by ZFMISC_1:96; then A3: dom (mlt (x1,x2)) = (dom x1) /\ (dom x2) by A2, FUNCOP_1:69; then i in dom x2 by A1, XBOOLE_0:def_4; then A4: x2 /. i = x2 . i by PARTFUN1:def_6; i in dom x1 by A1, A3, XBOOLE_0:def_4; then x1 /. i = x1 . i by PARTFUN1:def_6; hence (mlt (x1,x2)) . i = (x1 /. i) * (x2 /. i) by A4, RVSUM_1:59; ::_thesis: (mlt (x1,x2)) /. i = (x1 /. i) * (x2 /. i) hence (mlt (x1,x2)) /. i = (x1 /. i) * (x2 /. i) by A1, PARTFUN1:def_6; ::_thesis: verum end; theorem Th14: :: MFOLD_2:14 for x1, x2, y1, y2 being FinSequence of REAL st len x1 = len x2 & len y1 = len y2 holds mlt ((x1 ^ y1),(x2 ^ y2)) = (mlt (x1,x2)) ^ (mlt (y1,y2)) proof let x1, x2, y1, y2 be FinSequence of REAL ; ::_thesis: ( len x1 = len x2 & len y1 = len y2 implies mlt ((x1 ^ y1),(x2 ^ y2)) = (mlt (x1,x2)) ^ (mlt (y1,y2)) ) assume that A1: len x1 = len x2 and A2: len y1 = len y2 ; ::_thesis: mlt ((x1 ^ y1),(x2 ^ y2)) = (mlt (x1,x2)) ^ (mlt (y1,y2)) A3: multreal .: ((x1 ^ y1),(x2 ^ y2)) = multreal * <:(x1 ^ y1),(x2 ^ y2):> by FUNCOP_1:def_3; A4: dom (x1 ^ y1) = Seg (len (x1 ^ y1)) by FINSEQ_1:def_3; ( dom multreal = [:REAL,REAL:] & rng (x1 ^ y1) c= REAL ) by FUNCT_2:def_1; then [:(rng (x1 ^ y1)),(rng (x2 ^ y2)):] c= dom multreal by ZFMISC_1:96; then A5: dom (multreal * <:(x1 ^ y1),(x2 ^ y2):>) = (dom (x1 ^ y1)) /\ (dom (x2 ^ y2)) by A3, FUNCOP_1:69; A6: len (x2 ^ y2) = (len x2) + (len y2) by FINSEQ_1:22; dom (x2 ^ y2) = Seg (len (x2 ^ y2)) by FINSEQ_1:def_3; then dom (x1 ^ y1) = dom (x2 ^ y2) by A1, A2, A6, A4, FINSEQ_1:22; then A7: dom (mlt ((x1 ^ y1),(x2 ^ y2))) = dom (x1 ^ y1) by A3, A5, RVSUM_1:def_9; A8: multreal .: (y1,y2) = multreal * <:y1,y2:> by FUNCOP_1:def_3; A9: dom multreal = [:REAL,REAL:] by FUNCT_2:def_1; then [:(rng y1),(rng y2):] c= dom multreal by ZFMISC_1:96; then A10: dom (multreal * <:y1,y2:>) = (dom y1) /\ (dom y2) by A8, FUNCOP_1:69; dom y2 = Seg (len y1) by A2, FINSEQ_1:def_3 .= dom y1 by FINSEQ_1:def_3 ; then A11: dom (mlt (y1,y2)) = dom y1 by A8, A10, RVSUM_1:def_9; then dom (mlt (y1,y2)) = Seg (len y1) by FINSEQ_1:def_3; then A12: len (mlt (y1,y2)) = len y1 by FINSEQ_1:def_3; A13: multreal .: (x1,x2) = multreal * <:x1,x2:> by FUNCOP_1:def_3; [:(rng x1),(rng x2):] c= dom multreal by A9, ZFMISC_1:96; then A14: dom (multreal * <:x1,x2:>) = (dom x1) /\ (dom x2) by A13, FUNCOP_1:69; A15: len (x1 ^ y1) = (len x1) + (len y1) by FINSEQ_1:22; dom x2 = Seg (len x1) by A1, FINSEQ_1:def_3 .= dom x1 by FINSEQ_1:def_3 ; then A16: dom (mlt (x1,x2)) = dom x1 by A13, A14, RVSUM_1:def_9; then A17: dom (mlt (x1,x2)) = Seg (len x1) by FINSEQ_1:def_3; A18: for i being Nat st 1 <= i & i <= len (mlt ((x1 ^ y1),(x2 ^ y2))) holds (mlt ((x1 ^ y1),(x2 ^ y2))) . i = ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i proof let i be Nat; ::_thesis: ( 1 <= i & i <= len (mlt ((x1 ^ y1),(x2 ^ y2))) implies (mlt ((x1 ^ y1),(x2 ^ y2))) . i = ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i ) assume that A19: 1 <= i and A20: i <= len (mlt ((x1 ^ y1),(x2 ^ y2))) ; ::_thesis: (mlt ((x1 ^ y1),(x2 ^ y2))) . i = ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i i in Seg (len (mlt ((x1 ^ y1),(x2 ^ y2)))) by A19, A20, FINSEQ_1:1; then A21: i in dom (mlt ((x1 ^ y1),(x2 ^ y2))) by FINSEQ_1:def_3; then i <= len (x1 ^ y1) by A4, A7, FINSEQ_1:1; then A22: (x1 ^ y1) /. i = (x1 ^ y1) . i by A19, FINSEQ_4:15; i <= len (x2 ^ y2) by A1, A2, A15, A6, A4, A7, A21, FINSEQ_1:1; then A23: (x2 ^ y2) /. i = (x2 ^ y2) . i by A19, FINSEQ_4:15; A24: i <= (len x1) + (len y1) by A15, A4, A7, A21, FINSEQ_1:1; now__::_thesis:_((x1_^_y1)_/._i)_*_((x2_^_y2)_/._i)_=_((mlt_(x1,x2))_^_(mlt_(y1,y2)))_._i percases ( i <= len x1 or i > len x1 ) ; supposeA25: i <= len x1 ; ::_thesis: ((x1 ^ y1) /. i) * ((x2 ^ y2) /. i) = ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i then A26: i in Seg (len x1) by A19, FINSEQ_1:1; then A27: i in dom x1 by FINSEQ_1:def_3; i in dom x2 by A1, A26, FINSEQ_1:def_3; then A28: (x2 ^ y2) . i = x2 . i by FINSEQ_1:def_7; A29: i in dom (mlt (x1,x2)) by A16, A26, FINSEQ_1:def_3; then A30: ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i = (mlt (x1,x2)) . i by FINSEQ_1:def_7 .= (x1 /. i) * (x2 /. i) by A29, Th13 ; ( x1 /. i = x1 . i & x2 /. i = x2 . i ) by A1, A19, A25, FINSEQ_4:15; hence ((x1 ^ y1) /. i) * ((x2 ^ y2) /. i) = ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i by A22, A23, A27, A28, A30, FINSEQ_1:def_7; ::_thesis: verum end; supposeA31: i > len x1 ; ::_thesis: ((x1 ^ y1) /. i) * ((x2 ^ y2) /. i) = ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i i <= len (x2 ^ y2) by A1, A2, A15, A6, A4, A7, A21, FINSEQ_1:1; then A32: (x2 ^ y2) /. i = (x2 ^ y2) . i by A19, FINSEQ_4:15; i <= len (x1 ^ y1) by A4, A7, A21, FINSEQ_1:1; then A33: (x1 ^ y1) /. i = (x1 ^ y1) . i by A19, FINSEQ_4:15; set k = i -' (len x1); A34: i -' (len x1) = i - (len x1) by A31, XREAL_1:233; then A35: i = (len x1) + (i -' (len x1)) ; i - (len x1) <= ((len x1) + (len y1)) - (len x1) by A24, XREAL_1:13; then A36: i -' (len x1) <= len y1 by A31, XREAL_1:233; i -' (len x1) > 0 by A31, A34, XREAL_1:50; then (i -' (len x1)) + 1 > 0 + 1 by XREAL_1:6; then A37: 1 <= i -' (len x1) by NAT_1:13; then A38: i -' (len x1) in Seg (len y1) by A36; then A39: i -' (len x1) in dom (mlt (y1,y2)) by A11, FINSEQ_1:def_3; i = (len (mlt (x1,x2))) + (i -' (len x1)) by A17, A35, FINSEQ_1:def_3; then A40: ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i = (mlt (y1,y2)) . (i -' (len x1)) by A39, FINSEQ_1:def_7 .= (y1 /. (i -' (len x1))) * (y2 /. (i -' (len x1))) by A39, Th13 ; i -' (len x1) in dom y1 by A38, FINSEQ_1:def_3; then A41: (x1 ^ y1) . i = y1 . (i -' (len x1)) by A35, FINSEQ_1:def_7; i -' (len x1) in Seg (len y1) by A37, A36; then A42: i -' (len x1) in dom y2 by A2, FINSEQ_1:def_3; ( y1 /. (i -' (len x1)) = y1 . (i -' (len x1)) & y2 /. (i -' (len x1)) = y2 . (i -' (len x1)) ) by A2, A37, A36, FINSEQ_4:15; hence ((x1 ^ y1) /. i) * ((x2 ^ y2) /. i) = ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i by A1, A35, A42, A41, A33, A32, A40, FINSEQ_1:def_7; ::_thesis: verum end; end; end; hence (mlt ((x1 ^ y1),(x2 ^ y2))) . i = ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i by A21, Th13; ::_thesis: verum end; len (mlt ((x1 ^ y1),(x2 ^ y2))) = len (x1 ^ y1) by A4, A7, FINSEQ_1:def_3 .= (len x1) + (len y1) by FINSEQ_1:22 ; then len (mlt ((x1 ^ y1),(x2 ^ y2))) = (len (mlt (x1,x2))) + (len (mlt (y1,y2))) by A17, A12, FINSEQ_1:def_3; then len (mlt ((x1 ^ y1),(x2 ^ y2))) = len ((mlt (x1,x2)) ^ (mlt (y1,y2))) by FINSEQ_1:22; hence mlt ((x1 ^ y1),(x2 ^ y2)) = (mlt (x1,x2)) ^ (mlt (y1,y2)) by A18, FINSEQ_1:14; ::_thesis: verum end; theorem Th15: :: MFOLD_2:15 for x1, x2, y1, y2 being FinSequence of REAL st len x1 = len x2 & len y1 = len y2 holds |((x1 ^ y1),(x2 ^ y2))| = |(x1,x2)| + |(y1,y2)| proof let x1, x2, y1, y2 be FinSequence of REAL ; ::_thesis: ( len x1 = len x2 & len y1 = len y2 implies |((x1 ^ y1),(x2 ^ y2))| = |(x1,x2)| + |(y1,y2)| ) A1: Sum ((mlt (x1,x2)) ^ (mlt (y1,y2))) = (Sum (mlt (x1,x2))) + (Sum (mlt (y1,y2))) by RVSUM_1:75; assume ( len x1 = len x2 & len y1 = len y2 ) ; ::_thesis: |((x1 ^ y1),(x2 ^ y2))| = |(x1,x2)| + |(y1,y2)| then Sum (mlt ((x1 ^ y1),(x2 ^ y2))) = (Sum (mlt (x1,x2))) + (Sum (mlt (y1,y2))) by A1, Th14; then |((x1 ^ y1),(x2 ^ y2))| = (Sum (mlt (x1,x2))) + (Sum (mlt (y1,y2))) by RVSUM_1:def_16; then |((x1 ^ y1),(x2 ^ y2))| = (Sum (mlt (x1,x2))) + |(y1,y2)| by RVSUM_1:def_16; hence |((x1 ^ y1),(x2 ^ y2))| = |(x1,x2)| + |(y1,y2)| by RVSUM_1:def_16; ::_thesis: verum end; Lm1: for n being Nat holds the carrier of (RealVectSpace (Seg n)) = the carrier of (TOP-REAL n) proof let n be Nat; ::_thesis: the carrier of (RealVectSpace (Seg n)) = the carrier of (TOP-REAL n) reconsider D = REAL as non empty set ; A1: Funcs ((Seg n),D) = REAL n by FINSEQ_2:93; RealVectSpace (Seg n) = RLSStruct(# (Funcs ((Seg n),REAL)),(RealFuncZero (Seg n)),(RealFuncAdd (Seg n)),(RealFuncExtMult (Seg n)) #) by FUNCSDOM:def_6; hence the carrier of (RealVectSpace (Seg n)) = the carrier of (TOP-REAL n) by A1, EUCLID:22; ::_thesis: verum end; Lm2: for n being Nat holds 0. (RealVectSpace (Seg n)) = 0. (TOP-REAL n) proof let n be Nat; ::_thesis: 0. (RealVectSpace (Seg n)) = 0. (TOP-REAL n) RealVectSpace (Seg n) = RLSStruct(# (Funcs ((Seg n),REAL)),(RealFuncZero (Seg n)),(RealFuncAdd (Seg n)),(RealFuncExtMult (Seg n)) #) by FUNCSDOM:def_6; hence 0. (RealVectSpace (Seg n)) = (Seg n) --> 0 by FUNCSDOM:def_4 .= 0* n by FINSEQ_2:def_2 .= 0. (TOP-REAL n) by EUCLID:70 ; ::_thesis: verum end; theorem Th16: :: MFOLD_2:16 for k, n being Nat for p1, p2 being Point of (TOP-REAL n) st k in Seg n holds (p1 + p2) . k = (p1 . k) + (p2 . k) proof let k, n be Nat; ::_thesis: for p1, p2 being Point of (TOP-REAL n) st k in Seg n holds (p1 + p2) . k = (p1 . k) + (p2 . k) let p1, p2 be Point of (TOP-REAL n); ::_thesis: ( k in Seg n implies (p1 + p2) . k = (p1 . k) + (p2 . k) ) A1: dom (p1 + p2) = Seg n by FINSEQ_1:89; thus ( k in Seg n implies (p1 + p2) . k = (p1 . k) + (p2 . k) ) by A1, VALUED_1:def_1; ::_thesis: verum end; theorem Th17: :: MFOLD_2:17 for n being Nat for X being set holds ( X is Linear_Combination of RealVectSpace (Seg n) iff X is Linear_Combination of TOP-REAL n ) proof let n be Nat; ::_thesis: for X being set holds ( X is Linear_Combination of RealVectSpace (Seg n) iff X is Linear_Combination of TOP-REAL n ) let X be set ; ::_thesis: ( X is Linear_Combination of RealVectSpace (Seg n) iff X is Linear_Combination of TOP-REAL n ) set V = RealVectSpace (Seg n); set T = TOP-REAL n; hereby ::_thesis: ( X is Linear_Combination of TOP-REAL n implies X is Linear_Combination of RealVectSpace (Seg n) ) assume X is Linear_Combination of RealVectSpace (Seg n) ; ::_thesis: X is Linear_Combination of TOP-REAL n then reconsider L = X as Linear_Combination of RealVectSpace (Seg n) ; consider S being finite Subset of (RealVectSpace (Seg n)) such that A1: for v being Element of (RealVectSpace (Seg n)) st not v in S holds L . v = 0 by RLVECT_2:def_3; A2: now__::_thesis:_for_v_being_Element_of_(TOP-REAL_n)_st_not_v_in_S_holds_ 0_=_L_._v let v be Element of (TOP-REAL n); ::_thesis: ( not v in S implies 0 = L . v ) assume A3: not v in S ; ::_thesis: 0 = L . v v is Element of (RealVectSpace (Seg n)) by Lm1; hence 0 = L . v by A1, A3; ::_thesis: verum end; ( L is Element of Funcs ( the carrier of (TOP-REAL n),REAL) & S is finite Subset of (TOP-REAL n) ) by Lm1; hence X is Linear_Combination of TOP-REAL n by A2, RLVECT_2:def_3; ::_thesis: verum end; assume X is Linear_Combination of TOP-REAL n ; ::_thesis: X is Linear_Combination of RealVectSpace (Seg n) then reconsider L = X as Linear_Combination of TOP-REAL n ; consider S being finite Subset of (TOP-REAL n) such that A4: for v being Element of (TOP-REAL n) st not v in S holds L . v = 0 by RLVECT_2:def_3; A5: now__::_thesis:_for_v_being_Element_of_(RealVectSpace_(Seg_n))_st_not_v_in_S_holds_ 0_=_L_._v let v be Element of (RealVectSpace (Seg n)); ::_thesis: ( not v in S implies 0 = L . v ) assume A6: not v in S ; ::_thesis: 0 = L . v v is Element of (TOP-REAL n) by Lm1; hence 0 = L . v by A4, A6; ::_thesis: verum end; ( L is Element of Funcs ( the carrier of (RealVectSpace (Seg n)),REAL) & S is finite Subset of (RealVectSpace (Seg n)) ) by Lm1; hence X is Linear_Combination of RealVectSpace (Seg n) by A5, RLVECT_2:def_3; ::_thesis: verum end; theorem Th18: :: MFOLD_2:18 for n being Nat for F being FinSequence of (TOP-REAL n) for fr being Function of (TOP-REAL n),REAL for Fv being FinSequence of (RealVectSpace (Seg n)) for fv being Function of (RealVectSpace (Seg n)),REAL st fr = fv & F = Fv holds fr (#) F = fv (#) Fv proof let n be Nat; ::_thesis: for F being FinSequence of (TOP-REAL n) for fr being Function of (TOP-REAL n),REAL for Fv being FinSequence of (RealVectSpace (Seg n)) for fv being Function of (RealVectSpace (Seg n)),REAL st fr = fv & F = Fv holds fr (#) F = fv (#) Fv let F be FinSequence of (TOP-REAL n); ::_thesis: for fr being Function of (TOP-REAL n),REAL for Fv being FinSequence of (RealVectSpace (Seg n)) for fv being Function of (RealVectSpace (Seg n)),REAL st fr = fv & F = Fv holds fr (#) F = fv (#) Fv let fr be Function of (TOP-REAL n),REAL; ::_thesis: for Fv being FinSequence of (RealVectSpace (Seg n)) for fv being Function of (RealVectSpace (Seg n)),REAL st fr = fv & F = Fv holds fr (#) F = fv (#) Fv let Fv be FinSequence of (RealVectSpace (Seg n)); ::_thesis: for fv being Function of (RealVectSpace (Seg n)),REAL st fr = fv & F = Fv holds fr (#) F = fv (#) Fv let fv be Function of (RealVectSpace (Seg n)),REAL; ::_thesis: ( fr = fv & F = Fv implies fr (#) F = fv (#) Fv ) assume that A1: fr = fv and A2: F = Fv ; ::_thesis: fr (#) F = fv (#) Fv A3: len (fv (#) Fv) = len Fv by RLVECT_2:def_7; A4: len (fr (#) F) = len F by RLVECT_2:def_7; now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_F_holds_ (fr_(#)_F)_._i_=_(fv_(#)_Fv)_._i reconsider T = TOP-REAL n as RealLinearSpace ; let i be Nat; ::_thesis: ( 1 <= i & i <= len F implies (fr (#) F) . i = (fv (#) Fv) . i ) reconsider Fi = F /. i as FinSequence of REAL by EUCLID:24; A5: the carrier of (n -VectSp_over F_Real) = the carrier of (TOP-REAL n) proof thus the carrier of (n -VectSp_over F_Real) = REAL n by MATRIX13:102 .= the carrier of (TOP-REAL n) by EUCLID:22 ; ::_thesis: verum end; the carrier of (n -VectSp_over F_Real) = n -tuples_on the carrier of F_Real by MATRIX13:102; then reconsider Fvi = Fv /. i as Element of n -tuples_on the carrier of F_Real by Lm1, A5; reconsider Fii = F /. i as Element of T ; assume A6: ( 1 <= i & i <= len F ) ; ::_thesis: (fr (#) F) . i = (fv (#) Fv) . i then A7: i in dom (fv (#) Fv) by A2, A3, FINSEQ_3:25; i in dom F by A6, FINSEQ_3:25; then A8: F /. i = F . i by PARTFUN1:def_6; i in dom Fv by A2, A6, FINSEQ_3:25; then A9: Fv /. i = Fv . i by PARTFUN1:def_6; i in dom (fr (#) F) by A4, A6, FINSEQ_3:25; hence (fr (#) F) . i = (fr . Fii) * Fii by RLVECT_2:def_7 .= (fv . (Fv /. i)) * (Fv /. i) by A1, A2, A8, A9, EUCLID:65 .= (fv (#) Fv) . i by A7, RLVECT_2:def_7 ; ::_thesis: verum end; hence fr (#) F = fv (#) Fv by A2, A4, A3, FINSEQ_1:14; ::_thesis: verum end; theorem Th19: :: MFOLD_2:19 for n being Nat for F being FinSequence of (TOP-REAL n) for Fv being FinSequence of (RealVectSpace (Seg n)) st Fv = F holds Sum F = Sum Fv proof let n be Nat; ::_thesis: for F being FinSequence of (TOP-REAL n) for Fv being FinSequence of (RealVectSpace (Seg n)) st Fv = F holds Sum F = Sum Fv set T = TOP-REAL n; set V = RealVectSpace (Seg n); let F be FinSequence of (TOP-REAL n); ::_thesis: for Fv being FinSequence of (RealVectSpace (Seg n)) st Fv = F holds Sum F = Sum Fv let Fv be FinSequence of (RealVectSpace (Seg n)); ::_thesis: ( Fv = F implies Sum F = Sum Fv ) assume A1: Fv = F ; ::_thesis: Sum F = Sum Fv reconsider T = TOP-REAL n as RealLinearSpace ; consider f being Function of NAT, the carrier of T such that A2: Sum F = f . (len F) and A3: f . 0 = 0. T and A4: for j being Element of NAT for v being Element of T st j < len F & v = F . (j + 1) holds f . (j + 1) = (f . j) + v by RLVECT_1:def_12; consider fv being Function of NAT, the carrier of (RealVectSpace (Seg n)) such that A5: Sum Fv = fv . (len Fv) and A6: fv . 0 = 0. (RealVectSpace (Seg n)) and A7: for j being Element of NAT for v being Element of (RealVectSpace (Seg n)) st j < len Fv & v = Fv . (j + 1) holds fv . (j + 1) = (fv . j) + v by RLVECT_1:def_12; defpred S1[ Nat] means ( \$1 <= len F implies f . \$1 = fv . \$1 ); A8: for i being Element of NAT st S1[i] holds S1[i + 1] proof let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] ) assume A9: S1[i] ; ::_thesis: S1[i + 1] set i1 = i + 1; A10: the carrier of (n -VectSp_over F_Real) = the carrier of (TOP-REAL n) proof thus the carrier of (n -VectSp_over F_Real) = REAL n by MATRIX13:102 .= the carrier of (TOP-REAL n) by EUCLID:22 ; ::_thesis: verum end; the carrier of (n -VectSp_over F_Real) = n -tuples_on the carrier of F_Real by MATRIX13:102; then reconsider Fvi1 = Fv /. (i + 1), fvi = fv . i as Element of n -tuples_on the carrier of F_Real by A10, Lm1; reconsider Fi1 = F /. (i + 1) as Element of T ; assume A11: i + 1 <= len F ; ::_thesis: f . (i + 1) = fv . (i + 1) then A12: i < len F by NAT_1:13; 1 <= i + 1 by NAT_1:11; then A13: i + 1 in dom F by A11, FINSEQ_3:25; then F . (i + 1) = F /. (i + 1) by PARTFUN1:def_6; then A14: f . (i + 1) = (f . i) + Fi1 by A4, A12; A15: Fv /. (i + 1) = Fv . (i + 1) by A1, A13, PARTFUN1:def_6; then Fvi1 = F /. (i + 1) by A1, A13, PARTFUN1:def_6; hence f . (i + 1) = (fv . i) + (Fv /. (i + 1)) by A9, A11, A14, EUCLID:64, NAT_1:13 .= fv . (i + 1) by A1, A7, A12, A15 ; ::_thesis: verum end; A16: S1[ 0 ] by A3, A6, Lm2; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A16, A8); hence Sum F = Sum Fv by A1, A2, A5; ::_thesis: verum end; theorem Th20: :: MFOLD_2:20 for n being Nat for Lv being Linear_Combination of RealVectSpace (Seg n) for Lr being Linear_Combination of TOP-REAL n st Lr = Lv holds Sum Lr = Sum Lv proof let n be Nat; ::_thesis: for Lv being Linear_Combination of RealVectSpace (Seg n) for Lr being Linear_Combination of TOP-REAL n st Lr = Lv holds Sum Lr = Sum Lv set V = RealVectSpace (Seg n); set T = TOP-REAL n; let Lv be Linear_Combination of RealVectSpace (Seg n); ::_thesis: for Lr being Linear_Combination of TOP-REAL n st Lr = Lv holds Sum Lr = Sum Lv let Lr be Linear_Combination of TOP-REAL n; ::_thesis: ( Lr = Lv implies Sum Lr = Sum Lv ) assume A1: Lr = Lv ; ::_thesis: Sum Lr = Sum Lv consider F being FinSequence of the carrier of (TOP-REAL n) such that A2: ( F is one-to-one & rng F = Carrier Lr ) and A3: Sum Lr = Sum (Lr (#) F) by RLVECT_2:def_8; reconsider F1 = F as FinSequence of the carrier of (RealVectSpace (Seg n)) by Lm1; A4: Lr (#) F = Lv (#) F1 by A1, Th18; thus Sum Lv = Sum (Lv (#) F1) by A1, A2, RLVECT_2:def_8 .= Sum Lr by A3, A4, Th19 ; ::_thesis: verum end; theorem Th21: :: MFOLD_2:21 for n being Nat for Af being Subset of (RealVectSpace (Seg n)) for Ar being Subset of (TOP-REAL n) st Af = Ar holds ( Af is linearly-independent iff Ar is linearly-independent ) proof let n be Nat; ::_thesis: for Af being Subset of (RealVectSpace (Seg n)) for Ar being Subset of (TOP-REAL n) st Af = Ar holds ( Af is linearly-independent iff Ar is linearly-independent ) set V = RealVectSpace (Seg n); let AV be Subset of (RealVectSpace (Seg n)); ::_thesis: for Ar being Subset of (TOP-REAL n) st AV = Ar holds ( AV is linearly-independent iff Ar is linearly-independent ) set T = TOP-REAL n; let AR be Subset of (TOP-REAL n); ::_thesis: ( AV = AR implies ( AV is linearly-independent iff AR is linearly-independent ) ) assume A1: AV = AR ; ::_thesis: ( AV is linearly-independent iff AR is linearly-independent ) hereby ::_thesis: ( AR is linearly-independent implies AV is linearly-independent ) assume A2: AV is linearly-independent ; ::_thesis: AR is linearly-independent now__::_thesis:_for_L_being_Linear_Combination_of_AR_st_Sum_L_=_0._(TOP-REAL_n)_holds_ Carrier_L_=_{} let L be Linear_Combination of AR; ::_thesis: ( Sum L = 0. (TOP-REAL n) implies Carrier L = {} ) reconsider L1 = L as Linear_Combination of RealVectSpace (Seg n) by Th17; assume Sum L = 0. (TOP-REAL n) ; ::_thesis: Carrier L = {} then A3: 0. (RealVectSpace (Seg n)) = Sum L by Lm2 .= Sum L1 by Th20 ; Carrier L c= AR by RLVECT_2:def_6; then L1 is Linear_Combination of AV by A1, RLVECT_2:def_6; hence Carrier L = {} by A2, A3, RLVECT_3:def_1; ::_thesis: verum end; hence AR is linearly-independent by RLVECT_3:def_1; ::_thesis: verum end; assume A4: AR is linearly-independent ; ::_thesis: AV is linearly-independent now__::_thesis:_for_L_being_Linear_Combination_of_AV_st_Sum_L_=_0._(RealVectSpace_(Seg_n))_holds_ Carrier_L_=_{} let L be Linear_Combination of AV; ::_thesis: ( Sum L = 0. (RealVectSpace (Seg n)) implies Carrier L = {} ) reconsider L1 = L as Linear_Combination of TOP-REAL n by Th17; Carrier L c= AV by RLVECT_2:def_6; then reconsider L1 = L1 as Linear_Combination of AR by A1, RLVECT_2:def_6; assume Sum L = 0. (RealVectSpace (Seg n)) ; ::_thesis: Carrier L = {} then 0. (TOP-REAL n) = Sum L by Lm2 .= Sum L1 by Th20 ; hence Carrier L = {} by A4, RLVECT_3:def_1; ::_thesis: verum end; hence AV is linearly-independent by RLVECT_3:def_1; ::_thesis: verum end; theorem Th22: :: MFOLD_2:22 for n being Nat for p being Point of (TOP-REAL n) for V being Subset of (TOP-REAL n) st V = RN_Base n holds ex l being Linear_Combination of V st p = Sum l proof let n be Nat; ::_thesis: for p being Point of (TOP-REAL n) for V being Subset of (TOP-REAL n) st V = RN_Base n holds ex l being Linear_Combination of V st p = Sum l let p be Point of (TOP-REAL n); ::_thesis: for V being Subset of (TOP-REAL n) st V = RN_Base n holds ex l being Linear_Combination of V st p = Sum l let V be Subset of (TOP-REAL n); ::_thesis: ( V = RN_Base n implies ex l being Linear_Combination of V st p = Sum l ) assume A1: V = RN_Base n ; ::_thesis: ex l being Linear_Combination of V st p = Sum l reconsider p0 = p as Element of (RealVectSpace (Seg n)) by Lm1; reconsider V0 = V as Subset of (RealVectSpace (Seg n)) by Lm1; consider l0 being Linear_Combination of V0 such that A2: p0 = Sum l0 by A1, EUCLID_7:43; reconsider l = l0 as Linear_Combination of TOP-REAL n by Th17; Carrier l0 c= V0 by RLVECT_2:def_6; then reconsider l = l as Linear_Combination of V by RLVECT_2:def_6; take l ; ::_thesis: p = Sum l thus p = Sum l by A2, Th20; ::_thesis: verum end; theorem :: MFOLD_2:23 for n being Nat holds RN_Base n is Basis of TOP-REAL n proof let n be Nat; ::_thesis: RN_Base n is Basis of TOP-REAL n set A = RN_Base n; set T = TOP-REAL n; RN_Base n c= REAL n ; then A1: RN_Base n c= the carrier of (TOP-REAL n) by EUCLID:22; reconsider A = RN_Base n as finite Subset of (TOP-REAL n) by EUCLID:22; reconsider B = RN_Base n as Subset of (RealVectSpace (Seg n)) by A1, Lm1; B is Basis of RealVectSpace (Seg n) by EUCLID_7:45; then B is linearly-independent by RLVECT_3:def_3; then A2: A is linearly-independent by Th21; reconsider V1 = (Omega). (TOP-REAL n) as RealLinearSpace ; for v being VECTOR of (TOP-REAL n) st v in Lin A holds v in V1 proof let v be VECTOR of (TOP-REAL n); ::_thesis: ( v in Lin A implies v in V1 ) assume v in Lin A ; ::_thesis: v in V1 v in RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the U5 of (TOP-REAL n), the Mult of (TOP-REAL n) #) by STRUCT_0:def_5; hence v in V1 by RLSUB_1:def_4; ::_thesis: verum end; then reconsider X = Lin A as Subspace of V1 by RLSUB_1:29; for x being set holds ( x in the carrier of X iff x in the carrier of V1 ) proof let x be set ; ::_thesis: ( x in the carrier of X iff x in the carrier of V1 ) hereby ::_thesis: ( x in the carrier of V1 implies x in the carrier of X ) assume x in the carrier of X ; ::_thesis: x in the carrier of V1 then x in X by STRUCT_0:def_5; then x in V1 by RLSUB_1:9; hence x in the carrier of V1 by STRUCT_0:def_5; ::_thesis: verum end; assume x in the carrier of V1 ; ::_thesis: x in the carrier of X then x in (Omega). (TOP-REAL n) by STRUCT_0:def_5; then x in RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the U5 of (TOP-REAL n), the Mult of (TOP-REAL n) #) by RLSUB_1:def_4; then reconsider x0 = x as Element of (TOP-REAL n) by STRUCT_0:def_5; ex l being Linear_Combination of A st x0 = Sum l by Th22; then x in { (Sum l) where l is Linear_Combination of A : verum } ; hence x in the carrier of X by RLVECT_3:def_2; ::_thesis: verum end; then the carrier of X = the carrier of V1 by TARSKI:1; then Lin A = (Omega). (TOP-REAL n) by EUCLID_7:9; then Lin A = RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the U5 of (TOP-REAL n), the Mult of (TOP-REAL n) #) by RLSUB_1:def_4; hence RN_Base n is Basis of TOP-REAL n by A2, RLVECT_3:def_3; ::_thesis: verum end; theorem Th24: :: MFOLD_2:24 for n being Nat for V being Subset of (TOP-REAL n) holds ( V in the topology of (TOP-REAL n) iff for p being Point of (TOP-REAL n) st p in V holds ex r being real number st ( r > 0 & Ball (p,r) c= V ) ) proof let n be Nat; ::_thesis: for V being Subset of (TOP-REAL n) holds ( V in the topology of (TOP-REAL n) iff for p being Point of (TOP-REAL n) st p in V holds ex r being real number st ( r > 0 & Ball (p,r) c= V ) ) let V be Subset of (TOP-REAL n); ::_thesis: ( V in the topology of (TOP-REAL n) iff for p being Point of (TOP-REAL n) st p in V holds ex r being real number st ( r > 0 & Ball (p,r) c= V ) ) reconsider n1 = n as Element of NAT by ORDINAL1:def_12; set T = TOP-REAL n; A1: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8; A2: TopSpaceMetr (Euclid n) = TopStruct(# the carrier of (Euclid n),(Family_open_set (Euclid n)) #) by PCOMPS_1:def_5; reconsider V1 = V as Subset of (Euclid n) by EUCLID:67; hereby ::_thesis: ( ( for p being Point of (TOP-REAL n) st p in V holds ex r being real number st ( r > 0 & Ball (p,r) c= V ) ) implies V in the topology of (TOP-REAL n) ) assume A3: V in the topology of (TOP-REAL n) ; ::_thesis: for p being Point of (TOP-REAL n) st p in V holds ex r being real number st ( r > 0 & Ball (p,r) c= V ) let p be Point of (TOP-REAL n); ::_thesis: ( p in V implies ex r being real number st ( r > 0 & Ball (p,r) c= V ) ) assume A4: p in V ; ::_thesis: ex r being real number st ( r > 0 & Ball (p,r) c= V ) reconsider x = p as Element of (Euclid n) by EUCLID:67; consider r being Real such that A5: ( r > 0 & Ball (x,r) c= V1 ) by A3, A4, A1, A2, PCOMPS_1:def_4; reconsider r = r as real number ; take r = r; ::_thesis: ( r > 0 & Ball (p,r) c= V ) thus r > 0 by A5; ::_thesis: Ball (p,r) c= V reconsider x1 = x as Point of (Euclid n1) ; reconsider p1 = p as Point of (TOP-REAL n1) ; Ball (x1,r) = Ball (p1,r) by TOPREAL9:13; hence Ball (p,r) c= V by A5; ::_thesis: verum end; assume A6: for p being Point of (TOP-REAL n) st p in V holds ex r being real number st ( r > 0 & Ball (p,r) c= V ) ; ::_thesis: V in the topology of (TOP-REAL n) for x being Element of (Euclid n) st x in V1 holds ex r being Real st ( r > 0 & Ball (x,r) c= V1 ) proof let x be Element of (Euclid n); ::_thesis: ( x in V1 implies ex r being Real st ( r > 0 & Ball (x,r) c= V1 ) ) assume A7: x in V1 ; ::_thesis: ex r being Real st ( r > 0 & Ball (x,r) c= V1 ) reconsider p = x as Point of (TOP-REAL n) by EUCLID:67; consider r being real number such that A8: ( r > 0 & Ball (p,r) c= V ) by A6, A7; reconsider r = r as Real by XREAL_0:def_1; take r ; ::_thesis: ( r > 0 & Ball (x,r) c= V1 ) thus r > 0 by A8; ::_thesis: Ball (x,r) c= V1 reconsider x1 = x as Point of (Euclid n1) ; reconsider p1 = p as Point of (TOP-REAL n1) ; Ball (x1,r) = Ball (p1,r) by TOPREAL9:13; hence Ball (x,r) c= V1 by A8; ::_thesis: verum end; hence V in the topology of (TOP-REAL n) by A1, A2, PCOMPS_1:def_4; ::_thesis: verum end; definition let n be Nat; let p be Point of (TOP-REAL n); func InnerProduct p -> Function of (TOP-REAL n),R^1 means :Def1: :: MFOLD_2:def 1 for q being Point of (TOP-REAL n) holds it . q = |(p,q)|; existence ex b1 being Function of (TOP-REAL n),R^1 st for q being Point of (TOP-REAL n) holds b1 . q = |(p,q)| proof defpred S1[ set , set ] means ex q being Point of (TOP-REAL n) st ( q = \$1 & \$2 = |(p,q)| ); A1: for x being set st x in the carrier of (TOP-REAL n) holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in the carrier of (TOP-REAL n) implies ex y being set st S1[x,y] ) assume x in the carrier of (TOP-REAL n) ; ::_thesis: ex y being set st S1[x,y] then reconsider q3 = x as Point of (TOP-REAL n) ; take |(p,q3)| ; ::_thesis: S1[x,|(p,q3)|] thus S1[x,|(p,q3)|] ; ::_thesis: verum end; consider f1 being Function such that A2: ( dom f1 = the carrier of (TOP-REAL n) & ( for x being set st x in the carrier of (TOP-REAL n) holds S1[x,f1 . x] ) ) from CLASSES1:sch_1(A1); rng f1 c= the carrier of R^1 proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng f1 or z in the carrier of R^1 ) assume z in rng f1 ; ::_thesis: z in the carrier of R^1 then consider xz being set such that A3: xz in dom f1 and A4: z = f1 . xz by FUNCT_1:def_3; ex q4 being Point of (TOP-REAL n) st ( q4 = xz & f1 . xz = |(p,q4)| ) by A2, A3; hence z in the carrier of R^1 by A4, TOPMETR:17; ::_thesis: verum end; then reconsider f2 = f1 as Function of (TOP-REAL n),R^1 by A2, FUNCT_2:def_1, RELSET_1:4; take f2 ; ::_thesis: for q being Point of (TOP-REAL n) holds f2 . q = |(p,q)| for q being Point of (TOP-REAL n) holds f1 . q = |(p,q)| proof let q be Point of (TOP-REAL n); ::_thesis: f1 . q = |(p,q)| ex q2 being Point of (TOP-REAL n) st ( q2 = q & f1 . q = |(p,q2)| ) by A2; hence f1 . q = |(p,q)| ; ::_thesis: verum end; hence for q being Point of (TOP-REAL n) holds f2 . q = |(p,q)| ; ::_thesis: verum end; uniqueness for b1, b2 being Function of (TOP-REAL n),R^1 st ( for q being Point of (TOP-REAL n) holds b1 . q = |(p,q)| ) & ( for q being Point of (TOP-REAL n) holds b2 . q = |(p,q)| ) holds b1 = b2 proof let f1, f2 be Function of (TOP-REAL n),R^1; ::_thesis: ( ( for q being Point of (TOP-REAL n) holds f1 . q = |(p,q)| ) & ( for q being Point of (TOP-REAL n) holds f2 . q = |(p,q)| ) implies f1 = f2 ) assume that A5: for q being Point of (TOP-REAL n) holds f1 . q = |(p,q)| and A6: for q being Point of (TOP-REAL n) holds f2 . q = |(p,q)| ; ::_thesis: f1 = f2 for q being Point of (TOP-REAL n) holds f1 . q = f2 . q proof let q be Point of (TOP-REAL n); ::_thesis: f1 . q = f2 . q thus f1 . q = |(p,q)| by A5 .= f2 . q by A6 ; ::_thesis: verum end; hence f1 = f2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def1 defines InnerProduct MFOLD_2:def_1_:_ for n being Nat for p being Point of (TOP-REAL n) for b3 being Function of (TOP-REAL n),R^1 holds ( b3 = InnerProduct p iff for q being Point of (TOP-REAL n) holds b3 . q = |(p,q)| ); registration let n be Nat; let p be Point of (TOP-REAL n); cluster InnerProduct p -> continuous ; correctness coherence InnerProduct p is continuous ; proof set f = InnerProduct p; A1: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8; then reconsider f1 = InnerProduct p as Function of (TopSpaceMetr (Euclid n)),(TopSpaceMetr RealSpace) by TOPMETR:def_6; percases ( p = 0. (TOP-REAL n) or p <> 0. (TOP-REAL n) ) ; supposeA2: p = 0. (TOP-REAL n) ; ::_thesis: InnerProduct p is continuous A3: for q being Point of (TOP-REAL n) holds (InnerProduct p) . q = 0 proof let q be Point of (TOP-REAL n); ::_thesis: (InnerProduct p) . q = 0 (InnerProduct p) . q = |(q,p)| by Def1; hence (InnerProduct p) . q = 0 by A2, EUCLID_2:32; ::_thesis: verum end; consider g being Function of (TOP-REAL n),R^1 such that A4: ( ( for p being Point of (TOP-REAL n) holds g . p = 0 ) & g is continuous ) by JGRAPH_2:20; for x being set st x in the carrier of (TOP-REAL n) holds (InnerProduct p) . x = g . x proof let x be set ; ::_thesis: ( x in the carrier of (TOP-REAL n) implies (InnerProduct p) . x = g . x ) assume x in the carrier of (TOP-REAL n) ; ::_thesis: (InnerProduct p) . x = g . x then reconsider q = x as Point of (TOP-REAL n) ; thus (InnerProduct p) . x = (InnerProduct p) . q .= 0 by A3 .= g . q by A4 .= g . x ; ::_thesis: verum end; hence InnerProduct p is continuous by A4, FUNCT_2:12; ::_thesis: verum end; suppose p <> 0. (TOP-REAL n) ; ::_thesis: InnerProduct p is continuous then A5: |.p.| > 0 by EUCLID_2:44; reconsider n1 = n as Element of NAT by ORDINAL1:def_12; now__::_thesis:_for_r_being_real_number_ for_u_being_Element_of_(Euclid_n) for_u1_being_Element_of_RealSpace_st_r_>_0_&_u1_=_f1_._u_holds_ ex_s_being_real_number_st_ (_s_>_0_&_(_for_w_being_Element_of_(Euclid_n) for_w1_being_Element_of_RealSpace_st_w1_=_f1_._w_&_dist_(u,w)_<_s_holds_ dist_(u1,w1)_<_r_)_) let r be real number ; ::_thesis: for u being Element of (Euclid n) for u1 being Element of RealSpace st r > 0 & u1 = f1 . u holds ex s being real number st ( s > 0 & ( for w being Element of (Euclid n) for w1 being Element of RealSpace st w1 = f1 . w & dist (u,w) < s holds dist (u1,w1) < r ) ) let u be Element of (Euclid n); ::_thesis: for u1 being Element of RealSpace st r > 0 & u1 = f1 . u holds ex s being real number st ( s > 0 & ( for w being Element of (Euclid n) for w1 being Element of RealSpace st w1 = f1 . w & dist (u,w) < s holds dist (u1,w1) < r ) ) let u1 be Element of RealSpace; ::_thesis: ( r > 0 & u1 = f1 . u implies ex s being real number st ( s > 0 & ( for w being Element of (Euclid n) for w1 being Element of RealSpace st w1 = f1 . w & dist (u,w) < s holds dist (u1,w1) < r ) ) ) assume that A6: r > 0 and A7: u1 = f1 . u ; ::_thesis: ex s being real number st ( s > 0 & ( for w being Element of (Euclid n) for w1 being Element of RealSpace st w1 = f1 . w & dist (u,w) < s holds dist (u1,w1) < r ) ) set s1 = r / |.p.|; for w being Element of (Euclid n) for w1 being Element of RealSpace st w1 = f1 . w & dist (u,w) < r / |.p.| holds dist (u1,w1) < r proof let w be Element of (Euclid n); ::_thesis: for w1 being Element of RealSpace st w1 = f1 . w & dist (u,w) < r / |.p.| holds dist (u1,w1) < r let w1 be Element of RealSpace; ::_thesis: ( w1 = f1 . w & dist (u,w) < r / |.p.| implies dist (u1,w1) < r ) assume that A8: w1 = f1 . w and A9: dist (u,w) < r / |.p.| ; ::_thesis: dist (u1,w1) < r reconsider tu = u1, tw = w1 as Real by METRIC_1:def_13; reconsider qw = w, qu = u as Point of (TOP-REAL n1) by TOPREAL3:8; A10: dist (u1,w1) = the distance of RealSpace . (u1,w1) by METRIC_1:def_1 .= abs (tu - tw) by METRIC_1:def_12, METRIC_1:def_13 ; A11: w1 = |(qw,p)| by Def1, A8; abs (tu - tw) = abs (|(qu,p)| - |(qw,p)|) by Def1, A7, A11 .= abs |((qu - qw),p)| by EUCLID_2:24 ; then A12: dist (u1,w1) <= |.(qu - qw).| * |.p.| by A10, EUCLID_2:51; A13: (dist (u,w)) * |.p.| = |.(qu - qw).| * |.p.| by JGRAPH_1:28; (dist (u,w)) * |.p.| < (r / |.p.|) * |.p.| by A9, A5, XREAL_1:68; then (dist (u,w)) * |.p.| < r / (|.p.| / |.p.|) by XCMPLX_1:82; then (dist (u,w)) * |.p.| < r / 1 by A5, XCMPLX_1:60; hence dist (u1,w1) < r by A13, A12, XXREAL_0:2; ::_thesis: verum end; hence ex s being real number st ( s > 0 & ( for w being Element of (Euclid n) for w1 being Element of RealSpace st w1 = f1 . w & dist (u,w) < s holds dist (u1,w1) < r ) ) by A5, A6; ::_thesis: verum end; then f1 is continuous by UNIFORM1:3; hence InnerProduct p is continuous by A1, PRE_TOPC:32, TOPMETR:def_6; ::_thesis: verum end; end; end; end; begin definition let n be Nat; let p, q be Point of (TOP-REAL n); func Plane (p,q) -> Subset of (TOP-REAL n) equals :: MFOLD_2:def 2 { y where y is Point of (TOP-REAL n) : |(p,(y - q))| = 0 } ; correctness coherence { y where y is Point of (TOP-REAL n) : |(p,(y - q))| = 0 } is Subset of (TOP-REAL n); proof set X = { y where y is Point of (TOP-REAL n) : |(p,(y - q))| = 0 } ; now__::_thesis:_for_x_being_set_st_x_in__{__y_where_y_is_Point_of_(TOP-REAL_n)_:_|(p,(y_-_q))|_=_0__}__holds_ x_in_the_carrier_of_(TOP-REAL_n) let x be set ; ::_thesis: ( x in { y where y is Point of (TOP-REAL n) : |(p,(y - q))| = 0 } implies x in the carrier of (TOP-REAL n) ) assume x in { y where y is Point of (TOP-REAL n) : |(p,(y - q))| = 0 } ; ::_thesis: x in the carrier of (TOP-REAL n) then consider y being Point of (TOP-REAL n) such that A1: ( x = y & |(p,(y - q))| = 0 ) ; thus x in the carrier of (TOP-REAL n) by A1; ::_thesis: verum end; hence { y where y is Point of (TOP-REAL n) : |(p,(y - q))| = 0 } is Subset of (TOP-REAL n) by TARSKI:def_3; ::_thesis: verum end; end; :: deftheorem defines Plane MFOLD_2:def_2_:_ for n being Nat for p, q being Point of (TOP-REAL n) holds Plane (p,q) = { y where y is Point of (TOP-REAL n) : |(p,(y - q))| = 0 } ; theorem Th25: :: MFOLD_2:25 for n being Nat for p1, p, p2 being Point of (TOP-REAL n) holds (transl (p1,(TOP-REAL n))) .: (Plane (p,p2)) = Plane (p,(p1 + p2)) proof let n be Nat; ::_thesis: for p1, p, p2 being Point of (TOP-REAL n) holds (transl (p1,(TOP-REAL n))) .: (Plane (p,p2)) = Plane (p,(p1 + p2)) let p1, p, p2 be Point of (TOP-REAL n); ::_thesis: (transl (p1,(TOP-REAL n))) .: (Plane (p,p2)) = Plane (p,(p1 + p2)) A1: now__::_thesis:_for_y_being_set_st_y_in_(transl_(p1,(TOP-REAL_n)))_.:_(Plane_(p,p2))_holds_ y_in_Plane_(p,(p1_+_p2)) let y be set ; ::_thesis: ( y in (transl (p1,(TOP-REAL n))) .: (Plane (p,p2)) implies y in Plane (p,(p1 + p2)) ) assume y in (transl (p1,(TOP-REAL n))) .: (Plane (p,p2)) ; ::_thesis: y in Plane (p,(p1 + p2)) then consider x being set such that A2: ( [x,y] in transl (p1,(TOP-REAL n)) & x in Plane (p,p2) ) by RELAT_1:def_13; consider x1 being Point of (TOP-REAL n) such that A3: ( x = x1 & |(p,(x1 - p2))| = 0 ) by A2; A4: y = (transl (p1,(TOP-REAL n))) . x1 by A2, A3, FUNCT_1:1 .= p1 + x1 by RLTOPSP1:def_10 ; ( x in dom (transl (p1,(TOP-REAL n))) & y = (transl (p1,(TOP-REAL n))) . x ) by A2, FUNCT_1:1; then y in rng (transl (p1,(TOP-REAL n))) by FUNCT_1:3; then reconsider y1 = y as Point of (TOP-REAL n) ; x1 - p2 = (x1 - p2) + (0. (TOP-REAL n)) by EUCLID:27 .= (x1 - p2) + (p1 + (- p1)) by EUCLID:36 .= (x1 + (- p2)) + (p1 + (- p1)) by EUCLID:41 .= ((x1 + (- p2)) + p1) + (- p1) by EUCLID:26 .= (y1 + (- p2)) + (- p1) by A4, EUCLID:26 .= (y1 - p2) + (- p1) by EUCLID:41 .= (y1 - p2) - p1 by EUCLID:41 .= y1 - (p1 + p2) by EUCLID:46 ; hence y in Plane (p,(p1 + p2)) by A3; ::_thesis: verum end; now__::_thesis:_for_y_being_set_st_y_in_Plane_(p,(p1_+_p2))_holds_ y_in_(transl_(p1,(TOP-REAL_n)))_.:_(Plane_(p,p2)) let y be set ; ::_thesis: ( y in Plane (p,(p1 + p2)) implies y in (transl (p1,(TOP-REAL n))) .: (Plane (p,p2)) ) assume y in Plane (p,(p1 + p2)) ; ::_thesis: y in (transl (p1,(TOP-REAL n))) .: (Plane (p,p2)) then consider y1 being Point of (TOP-REAL n) such that A5: ( y = y1 & |(p,(y1 - (p1 + p2)))| = 0 ) ; set x = y1 - p1; y1 - p1 in the carrier of (TOP-REAL n) ; then A6: y1 - p1 in dom (transl (p1,(TOP-REAL n))) by FUNCT_2:def_1; p1 + (y1 - p1) = y1 by EUCLID:48; then (transl (p1,(TOP-REAL n))) . (y1 - p1) = y1 by RLTOPSP1:def_10; then A7: [(y1 - p1),y1] in transl (p1,(TOP-REAL n)) by A6, FUNCT_1:1; (y1 - p1) - p2 = y1 - (p1 + p2) by EUCLID:46; then y1 - p1 in Plane (p,p2) by A5; hence y in (transl (p1,(TOP-REAL n))) .: (Plane (p,p2)) by A5, A7, RELAT_1:def_13; ::_thesis: verum end; hence (transl (p1,(TOP-REAL n))) .: (Plane (p,p2)) = Plane (p,(p1 + p2)) by A1, TARSKI:1; ::_thesis: verum end; theorem Th26: :: MFOLD_2:26 for n being Nat for p being Point of (TOP-REAL n) st p <> 0. (TOP-REAL n) holds ex A being linearly-independent Subset of (TOP-REAL n) st ( card A = n - 1 & [#] (Lin A) = Plane (p,(0. (TOP-REAL n))) ) proof let n be Nat; ::_thesis: for p being Point of (TOP-REAL n) st p <> 0. (TOP-REAL n) holds ex A being linearly-independent Subset of (TOP-REAL n) st ( card A = n - 1 & [#] (Lin A) = Plane (p,(0. (TOP-REAL n))) ) let p be Point of (TOP-REAL n); ::_thesis: ( p <> 0. (TOP-REAL n) implies ex A being linearly-independent Subset of (TOP-REAL n) st ( card A = n - 1 & [#] (Lin A) = Plane (p,(0. (TOP-REAL n))) ) ) assume A1: p <> 0. (TOP-REAL n) ; ::_thesis: ex A being linearly-independent Subset of (TOP-REAL n) st ( card A = n - 1 & [#] (Lin A) = Plane (p,(0. (TOP-REAL n))) ) reconsider n1 = n as Element of NAT by ORDINAL1:def_12; A2: 0. (TOP-REAL n) = - (0. (TOP-REAL n1)) by JGRAPH_5:10 .= - (0. (TOP-REAL n)) ; set V1 = Plane (p,(0. (TOP-REAL n))); |(p,(0. (TOP-REAL n)))| = 0 by EUCLID_2:32; then |(p,((0. (TOP-REAL n)) - (0. (TOP-REAL n))))| = 0 by EUCLID:42; then A3: 0. (TOP-REAL n) in Plane (p,(0. (TOP-REAL n))) ; A4: for v, u being VECTOR of (TOP-REAL n) st v in Plane (p,(0. (TOP-REAL n))) & u in Plane (p,(0. (TOP-REAL n))) holds v + u in Plane (p,(0. (TOP-REAL n))) proof let v, u be VECTOR of (TOP-REAL n); ::_thesis: ( v in Plane (p,(0. (TOP-REAL n))) & u in Plane (p,(0. (TOP-REAL n))) implies v + u in Plane (p,(0. (TOP-REAL n))) ) assume v in Plane (p,(0. (TOP-REAL n))) ; ::_thesis: ( not u in Plane (p,(0. (TOP-REAL n))) or v + u in Plane (p,(0. (TOP-REAL n))) ) then consider v1 being Point of (TOP-REAL n) such that A5: ( v = v1 & |(p,(v1 - (0. (TOP-REAL n))))| = 0 ) ; assume u in Plane (p,(0. (TOP-REAL n))) ; ::_thesis: v + u in Plane (p,(0. (TOP-REAL n))) then consider u1 being Point of (TOP-REAL n) such that A6: ( u = u1 & |(p,(u1 - (0. (TOP-REAL n))))| = 0 ) ; |(p,((v1 + u1) - (0. (TOP-REAL n))))| = |(p,(v1 + (u1 - (0. (TOP-REAL n)))))| by EUCLID:45 .= |(p,v1)| + |(p,(u1 - (0. (TOP-REAL n))))| by EUCLID_2:26 .= |(p,(v1 + (0. (TOP-REAL n))))| by A6, EUCLID:27 .= 0 by A5, A2, EUCLID:41 ; hence v + u in Plane (p,(0. (TOP-REAL n))) by A5, A6; ::_thesis: verum end; for a being Real for v being VECTOR of (TOP-REAL n) st v in Plane (p,(0. (TOP-REAL n))) holds a * v in Plane (p,(0. (TOP-REAL n))) proof let a be Real; ::_thesis: for v being VECTOR of (TOP-REAL n) st v in Plane (p,(0. (TOP-REAL n))) holds a * v in Plane (p,(0. (TOP-REAL n))) let v be VECTOR of (TOP-REAL n); ::_thesis: ( v in Plane (p,(0. (TOP-REAL n))) implies a * v in Plane (p,(0. (TOP-REAL n))) ) assume v in Plane (p,(0. (TOP-REAL n))) ; ::_thesis: a * v in Plane (p,(0. (TOP-REAL n))) then consider v1 being Point of (TOP-REAL n) such that A7: ( v = v1 & |(p,(v1 - (0. (TOP-REAL n))))| = 0 ) ; |(p,(a * (v1 - (0. (TOP-REAL n)))))| = a * 0 by A7, EUCLID_2:20; then |(p,((a * v1) - (a * (0. (TOP-REAL n)))))| = 0 by EUCLID:49; then |(p,((a * v1) - (0. (TOP-REAL n))))| = 0 by EUCLID:28; hence a * v in Plane (p,(0. (TOP-REAL n))) by A7; ::_thesis: verum end; then Plane (p,(0. (TOP-REAL n))) is linearly-closed by A4, RLSUB_1:def_1; then consider W being strict Subspace of TOP-REAL n such that A8: Plane (p,(0. (TOP-REAL n))) = the carrier of W by A3, RLSUB_1:35; set A1 = the Basis of W; A9: ( the Basis of W is linearly-independent & the carrier of (Lin the Basis of W) = the carrier of W ) by RLVECT_3:def_3; A10: [#] (Lin the Basis of W) = Plane (p,(0. (TOP-REAL n))) by A8, RLVECT_3:def_3; reconsider A = the Basis of W as linearly-independent Subset of (TOP-REAL n) by A9, RLVECT_5:14; take A ; ::_thesis: ( card A = n - 1 & [#] (Lin A) = Plane (p,(0. (TOP-REAL n))) ) reconsider A2 = {p} as linearly-independent Subset of (TOP-REAL n) by A1, RLVECT_3:8; A11: dim (Lin A2) = card A2 by RLVECT_5:29 .= 1 by CARD_1:30 ; for v being VECTOR of (TOP-REAL n) ex v1, v2 being VECTOR of (TOP-REAL n) st ( v1 in Lin A & v2 in Lin A2 & v = v1 + v2 ) proof let v be VECTOR of (TOP-REAL n); ::_thesis: ex v1, v2 being VECTOR of (TOP-REAL n) st ( v1 in Lin A & v2 in Lin A2 & v = v1 + v2 ) set a = |(p,v)| / |(p,p)|; set v2 = (|(p,v)| / |(p,p)|) * p; set v1 = v - ((|(p,v)| / |(p,p)|) * p); reconsider v1 = v - ((|(p,v)| / |(p,p)|) * p), v2 = (|(p,v)| / |(p,p)|) * p as VECTOR of (TOP-REAL n) ; take v1 ; ::_thesis: ex v2 being VECTOR of (TOP-REAL n) st ( v1 in Lin A & v2 in Lin A2 & v = v1 + v2 ) take v2 ; ::_thesis: ( v1 in Lin A & v2 in Lin A2 & v = v1 + v2 ) A12: |(p,p)| > 0 by A1, EUCLID_2:43; |(p,v1)| = |(p,v)| - |(p,v2)| by EUCLID_2:27 .= |(p,v)| - ((|(p,v)| / |(p,p)|) * |(p,p)|) by EUCLID_2:20 .= |(p,v)| - |(p,v)| by A12, XCMPLX_1:87 .= 0 ; then |(p,(v1 + (0. (TOP-REAL n))))| = 0 by EUCLID:27; then |(p,(v1 - (0. (TOP-REAL n))))| = 0 by A2, EUCLID:41; then v1 in [#] (Lin the Basis of W) by A10; then v1 in Lin the Basis of W by STRUCT_0:def_5; hence v1 in Lin A by RLVECT_5:20; ::_thesis: ( v2 in Lin A2 & v = v1 + v2 ) thus v2 in Lin A2 by RLVECT_4:8; ::_thesis: v = v1 + v2 thus v = v1 + v2 by EUCLID:48; ::_thesis: verum end; then A13: RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the U5 of (TOP-REAL n), the Mult of (TOP-REAL n) #) = (Lin A) + (Lin A2) by RLSUB_2:44; (Lin A) /\ (Lin A2) = (0). (TOP-REAL n) proof for v being VECTOR of (TOP-REAL n) holds ( v in (Lin A) /\ (Lin A2) iff v in (0). (TOP-REAL n) ) proof let v be VECTOR of (TOP-REAL n); ::_thesis: ( v in (Lin A) /\ (Lin A2) iff v in (0). (TOP-REAL n) ) hereby ::_thesis: ( v in (0). (TOP-REAL n) implies v in (Lin A) /\ (Lin A2) ) assume v in (Lin A) /\ (Lin A2) ; ::_thesis: v in (0). (TOP-REAL n) then A14: ( v in Lin A & v in Lin A2 ) by RLSUB_2:3; then consider a being Real such that A15: v = a * p by RLVECT_4:8; Lin the Basis of W = Lin A by RLVECT_5:20; then v in Plane (p,(0. (TOP-REAL n))) by A10, A14, STRUCT_0:def_5; then consider y being Point of (TOP-REAL n) such that A16: ( y = v & |(p,(y - (0. (TOP-REAL n))))| = 0 ) ; |(p,(v + (- (0. (TOP-REAL n)))))| = 0 by A16, EUCLID:41; then |(p,v)| = 0 by A2, EUCLID:27; then A17: a * |(p,p)| = 0 by A15, EUCLID_2:20; |(p,p)| > 0 by A1, EUCLID_2:43; then a = 0 by A17; then v = 0. (TOP-REAL n) by A15, EUCLID:29; hence v in (0). (TOP-REAL n) by RLVECT_3:29; ::_thesis: verum end; assume v in (0). (TOP-REAL n) ; ::_thesis: v in (Lin A) /\ (Lin A2) then v = 0. (TOP-REAL n) by RLVECT_3:29; hence v in (Lin A) /\ (Lin A2) by RLSUB_1:17; ::_thesis: verum end; hence (Lin A) /\ (Lin A2) = (0). (TOP-REAL n) by RLSUB_1:31; ::_thesis: verum end; then TOP-REAL n is_the_direct_sum_of Lin A, Lin A2 by A13, RLSUB_2:def_4; then dim (TOP-REAL n) = (dim (Lin A)) + (dim (Lin A2)) by RLVECT_5:37; then n = (dim (Lin A)) + 1 by A11, RLAFFIN3:4; hence card A = n - 1 by RLVECT_5:29; ::_thesis: [#] (Lin A) = Plane (p,(0. (TOP-REAL n))) thus [#] (Lin A) = Plane (p,(0. (TOP-REAL n))) by A10, RLVECT_5:20; ::_thesis: verum end; theorem Th27: :: MFOLD_2:27 for n being Nat for p1, p2 being Point of (TOP-REAL n) st p1 <> 0. (TOP-REAL n) & p2 <> 0. (TOP-REAL n) holds ex R being Function of (TOP-REAL n),(TOP-REAL n) st ( R is being_homeomorphism & R .: (Plane (p1,(0. (TOP-REAL n)))) = Plane (p2,(0. (TOP-REAL n))) ) proof let n be Nat; ::_thesis: for p1, p2 being Point of (TOP-REAL n) st p1 <> 0. (TOP-REAL n) & p2 <> 0. (TOP-REAL n) holds ex R being Function of (TOP-REAL n),(TOP-REAL n) st ( R is being_homeomorphism & R .: (Plane (p1,(0. (TOP-REAL n)))) = Plane (p2,(0. (TOP-REAL n))) ) let p1, p2 be Point of (TOP-REAL n); ::_thesis: ( p1 <> 0. (TOP-REAL n) & p2 <> 0. (TOP-REAL n) implies ex R being Function of (TOP-REAL n),(TOP-REAL n) st ( R is being_homeomorphism & R .: (Plane (p1,(0. (TOP-REAL n)))) = Plane (p2,(0. (TOP-REAL n))) ) ) assume p1 <> 0. (TOP-REAL n) ; ::_thesis: ( not p2 <> 0. (TOP-REAL n) or ex R being Function of (TOP-REAL n),(TOP-REAL n) st ( R is being_homeomorphism & R .: (Plane (p1,(0. (TOP-REAL n)))) = Plane (p2,(0. (TOP-REAL n))) ) ) then consider B1 being linearly-independent Subset of (TOP-REAL n) such that A1: ( card B1 = n - 1 & [#] (Lin B1) = Plane (p1,(0. (TOP-REAL n))) ) by Th26; assume p2 <> 0. (TOP-REAL n) ; ::_thesis: ex R being Function of (TOP-REAL n),(TOP-REAL n) st ( R is being_homeomorphism & R .: (Plane (p1,(0. (TOP-REAL n)))) = Plane (p2,(0. (TOP-REAL n))) ) then consider B2 being linearly-independent Subset of (TOP-REAL n) such that A2: ( card B2 = n - 1 & [#] (Lin B2) = Plane (p2,(0. (TOP-REAL n))) ) by Th26; consider M being Matrix of n,F_Real such that A3: ( M is invertible & (Mx2Tran M) .: ([#] (Lin B1)) = [#] (Lin B2) ) by A1, A2, MATRTOP2:22; reconsider M = M as invertible Matrix of n,F_Real by A3; take Mx2Tran M ; ::_thesis: ( Mx2Tran M is being_homeomorphism & (Mx2Tran M) .: (Plane (p1,(0. (TOP-REAL n)))) = Plane (p2,(0. (TOP-REAL n))) ) thus ( Mx2Tran M is being_homeomorphism & (Mx2Tran M) .: (Plane (p1,(0. (TOP-REAL n)))) = Plane (p2,(0. (TOP-REAL n))) ) by A1, A2, A3; ::_thesis: verum end; definition let n be Nat; let p, q be Point of (TOP-REAL n); func TPlane (p,q) -> non empty SubSpace of TOP-REAL n equals :: MFOLD_2:def 3 (TOP-REAL n) | (Plane (p,q)); correctness coherence (TOP-REAL n) | (Plane (p,q)) is non empty SubSpace of TOP-REAL n; proof |(p,(0. (TOP-REAL n)))| = 0 by EUCLID_2:32; then |(p,(q - q))| = 0 by EUCLID:42; then q in Plane (p,q) ; hence (TOP-REAL n) | (Plane (p,q)) is non empty SubSpace of TOP-REAL n ; ::_thesis: verum end; end; :: deftheorem defines TPlane MFOLD_2:def_3_:_ for n being Nat for p, q being Point of (TOP-REAL n) holds TPlane (p,q) = (TOP-REAL n) | (Plane (p,q)); theorem Th28: :: MFOLD_2:28 for n being Nat holds Base_FinSeq ((n + 1),(n + 1)) = (0. (TOP-REAL n)) ^ <*1*> proof let n be Nat; ::_thesis: Base_FinSeq ((n + 1),(n + 1)) = (0. (TOP-REAL n)) ^ <*1*> set N = Base_FinSeq ((n + 1),(n + 1)); set p = 0. (TOP-REAL n); set q = <*1*>; A1: dom (Base_FinSeq ((n + 1),(n + 1))) = Seg (n + 1) by FINSEQ_1:89 .= Seg (n + (len <*1*>)) by FINSEQ_1:39 .= Seg ((len (0. (TOP-REAL n))) + (len <*1*>)) by CARD_1:def_7 ; A2: for k being Nat st k in dom (0. (TOP-REAL n)) holds (Base_FinSeq ((n + 1),(n + 1))) . k = (0. (TOP-REAL n)) . k proof let k be Nat; ::_thesis: ( k in dom (0. (TOP-REAL n)) implies (Base_FinSeq ((n + 1),(n + 1))) . k = (0. (TOP-REAL n)) . k ) assume k in dom (0. (TOP-REAL n)) ; ::_thesis: (Base_FinSeq ((n + 1),(n + 1))) . k = (0. (TOP-REAL n)) . k then k in Seg n by FINSEQ_1:89; then A3: ( 1 <= k & k <= n ) by FINSEQ_1:1; 0 + n <= 1 + n by XREAL_1:6; then A4: k <= n + 1 by A3, XXREAL_0:2; A5: n + 1 <> k by A3, NAT_1:13; thus (Base_FinSeq ((n + 1),(n + 1))) . k = 0 by A4, A3, A5, MATRIXR2:76 .= (0* n) . k .= (0. (TOP-REAL n)) . k by EUCLID:70 ; ::_thesis: verum end; for k being Nat st k in dom <*1*> holds (Base_FinSeq ((n + 1),(n + 1))) . ((len (0. (TOP-REAL n))) + k) = <*1*> . k proof let k be Nat; ::_thesis: ( k in dom <*1*> implies (Base_FinSeq ((n + 1),(n + 1))) . ((len (0. (TOP-REAL n))) + k) = <*1*> . k ) assume k in dom <*1*> ; ::_thesis: (Base_FinSeq ((n + 1),(n + 1))) . ((len (0. (TOP-REAL n))) + k) = <*1*> . k then k in {1} by FINSEQ_1:2, FINSEQ_1:38; then A6: k = 1 by TARSKI:def_1; A7: 0 + 1 <= n + 1 by XREAL_1:6; thus (Base_FinSeq ((n + 1),(n + 1))) . ((len (0. (TOP-REAL n))) + k) = (Base_FinSeq ((n + 1),(n + 1))) . (n + 1) by A6, CARD_1:def_7 .= 1 by A7, MATRIXR2:75 .= <*1*> . k by A6, FINSEQ_1:40 ; ::_thesis: verum end; hence Base_FinSeq ((n + 1),(n + 1)) = (0. (TOP-REAL n)) ^ <*1*> by A1, A2, FINSEQ_1:def_7; ::_thesis: verum end; 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 proof let n be Nat; ::_thesis: 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 let p0 be Point of (TOP-REAL (n + 1)); ::_thesis: ( p0 = Base_FinSeq ((n + 1),(n + 1)) implies TOP-REAL n, TPlane (p0,(0. (TOP-REAL (n + 1)))) are_homeomorphic ) assume A1: p0 = Base_FinSeq ((n + 1),(n + 1)) ; ::_thesis: TOP-REAL n, TPlane (p0,(0. (TOP-REAL (n + 1)))) are_homeomorphic set T = TOP-REAL n; set S = TPlane (p0,(0. (TOP-REAL (n + 1)))); defpred S1[ set , set ] means for p being Element of (TOP-REAL n) st \$1 = p holds \$2 = p ^ <*0*>; A2: for p being Element of (TOP-REAL n) holds p ^ <*0*> is Element of (TPlane (p0,(0. (TOP-REAL (n + 1))))) proof let p be Element of (TOP-REAL n); ::_thesis: p ^ <*0*> is Element of (TPlane (p0,(0. (TOP-REAL (n + 1))))) A3: len p = n by CARD_1:def_7; A4: len (p ^ <*0*>) = n + 1 by CARD_1:def_7; rng (p ^ <*0*>) c= REAL ; then p ^ <*0*> in REAL (n + 1) by A4, FINSEQ_2:132; then reconsider q = p ^ <*0*> as Point of (TOP-REAL (n + 1)) by EUCLID:22; reconsider r0 = 0 as Real by INT_1:3; ( dom p0 = Seg (n + 1) & dom q = Seg (n + 1) ) by FINSEQ_1:89; then (dom p0) /\ (dom q) = Seg (n + 1) ; then A5: dom (mlt (p0,q)) = Seg (n + 1) by VALUED_1:def_4; for y being set holds ( y in rng (mlt (p0,q)) iff y = r0 ) proof let y be set ; ::_thesis: ( y in rng (mlt (p0,q)) iff y = r0 ) set f = mlt (p0,q); A6: now__::_thesis:_for_x_being_set_st_x_in_Seg_(n_+_1)_holds_ (mlt_(p0,q))_._x_=_r0 let x be set ; ::_thesis: ( x in Seg (n + 1) implies (mlt (p0,q)) . b1 = r0 ) assume x in Seg (n + 1) ; ::_thesis: (mlt (p0,q)) . b1 = r0 then consider k being Element of NAT such that A7: ( x = k & 1 <= k & k <= n + 1 ) ; A8: (mlt (p0,q)) . x = (p0 . x) * (q . x) by VALUED_1:5; percases ( k = n + 1 or k <> n + 1 ) ; supposeA9: k = n + 1 ; ::_thesis: (mlt (p0,q)) . b1 = r0 1 <= len <*r0*> by FINSEQ_1:39; then q . ((len p) + 1) = <*r0*> . 1 by FINSEQ_1:65 .= r0 by FINSEQ_1:40 ; hence (mlt (p0,q)) . x = r0 by A8, A7, A9, A3; ::_thesis: verum end; suppose k <> n + 1 ; ::_thesis: (mlt (p0,q)) . b1 = r0 then p0 . x = 0 by A1, A7, MATRIXR2:76; hence (mlt (p0,q)) . x = r0 by A8; ::_thesis: verum end; end; end; hereby ::_thesis: ( y = r0 implies y in rng (mlt (p0,q)) ) assume y in rng (mlt (p0,q)) ; ::_thesis: y = r0 then consider x being set such that A10: ( x in dom (mlt (p0,q)) & y = (mlt (p0,q)) . x ) by FUNCT_1:def_3; thus y = r0 by A10, A5, A6; ::_thesis: verum end; assume A11: y = r0 ; ::_thesis: y in rng (mlt (p0,q)) consider x being set such that A12: x in Seg (n + 1) by XBOOLE_0:def_1; y = (mlt (p0,q)) . x by A11, A12, A6; hence y in rng (mlt (p0,q)) by A12, A5, FUNCT_1:def_3; ::_thesis: verum end; then A13: rng (mlt (p0,q)) = {r0} by TARSKI:def_1; mlt (p0,q) = (Seg (n + 1)) --> r0 by A13, A5, FUNCOP_1:9; then A14: mlt (p0,q) = (n + 1) |-> r0 by FINSEQ_2:def_2; A15: |(p0,q)| = Sum (mlt (p0,q)) by RVSUM_1:def_16 .= (n + 1) * r0 by A14, RVSUM_1:80 .= 0 ; |(p0,(q - (0. (TOP-REAL (n + 1)))))| = |(p0,q)| - |(p0,(0. (TOP-REAL (n + 1))))| by EUCLID_2:27 .= |(p0,q)| - 0 by EUCLID_2:32 .= 0 by A15 ; then p ^ <*0*> in Plane (p0,(0. (TOP-REAL (n + 1)))) ; then p ^ <*0*> in [#] (TPlane (p0,(0. (TOP-REAL (n + 1))))) by PRE_TOPC:def_5; hence p ^ <*0*> is Element of (TPlane (p0,(0. (TOP-REAL (n + 1))))) ; ::_thesis: verum end; A16: for x being Element of (TOP-REAL n) ex y being Element of (TPlane (p0,(0. (TOP-REAL (n + 1))))) st S1[x,y] proof let x be Element of (TOP-REAL n); ::_thesis: ex y being Element of (TPlane (p0,(0. (TOP-REAL (n + 1))))) st S1[x,y] set y = x ^ <*0*>; reconsider y = x ^ <*0*> as Element of (TPlane (p0,(0. (TOP-REAL (n + 1))))) by A2; take y ; ::_thesis: S1[x,y] thus S1[x,y] ; ::_thesis: verum end; consider f being Function of (TOP-REAL n),(TPlane (p0,(0. (TOP-REAL (n + 1))))) such that A17: for x being Element of (TOP-REAL n) holds S1[x,f . x] from FUNCT_2:sch_3(A16); A18: dom f = [#] (TOP-REAL n) by FUNCT_2:def_1; A19: for y being set holds ( y in [#] (TPlane (p0,(0. (TOP-REAL (n + 1))))) iff ex x being set st ( x in dom f & y = f . x ) ) proof let y be set ; ::_thesis: ( y in [#] (TPlane (p0,(0. (TOP-REAL (n + 1))))) iff ex x being set st ( x in dom f & y = f . x ) ) hereby ::_thesis: ( ex x being set st ( x in dom f & y = f . x ) implies y in [#] (TPlane (p0,(0. (TOP-REAL (n + 1))))) ) assume y in [#] (TPlane (p0,(0. (TOP-REAL (n + 1))))) ; ::_thesis: ex x being set st ( x in dom f & y = f . x ) then y in Plane (p0,(0. (TOP-REAL (n + 1)))) by PRE_TOPC:def_5; then consider q being Point of (TOP-REAL (n + 1)) such that A20: ( y = q & |(p0,(q - (0. (TOP-REAL (n + 1)))))| = 0 ) ; A21: ( len q = n + 1 & rng q c= REAL ) by CARD_1:def_7; then reconsider q1 = q as FinSequence of REAL by FINSEQ_1:def_4; set p = q1 | n; reconsider x = q1 | n as set ; take x = x; ::_thesis: ( x in dom f & y = f . x ) 0 + n <= 1 + n by XREAL_1:6; then A22: len (q1 | n) = n by A21, FINSEQ_1:59; A23: rng (q1 | n) c= REAL ; A24: q1 | n in REAL n by A22, A23, FINSEQ_2:132; hence x in dom f by A18, EUCLID:22; ::_thesis: y = f . x reconsider x1 = x as Element of (TOP-REAL n) by A24, EUCLID:22; S1[x1,f . x1] by A17; then A25: f . x = (q1 | n) ^ <*0*> ; A26: q = (q1 | n) ^ <*(q . (n + 1))*> by A21, FINSEQ_3:55; A27: |(p0,(q - (0. (TOP-REAL (n + 1)))))| = |(p0,q)| - |(p0,(0. (TOP-REAL (n + 1))))| by EUCLID_2:27 .= |(p0,q)| - 0 by EUCLID_2:32 .= |(p0,q)| ; reconsider f0 = 0. (TOP-REAL n) as FinSequence of REAL by EUCLID:24; rng <*1*> c= REAL ; then reconsider f1 = <*1*> as FinSequence of REAL by FINSEQ_1:def_4; reconsider f3 = <*(q . (n + 1))*> as FinSequence of REAL ; q1 | n in REAL n by A22, A23, FINSEQ_2:132; then reconsider p1 = q1 | n as Point of (TOP-REAL n) by EUCLID:22; A28: |((f0 ^ f1),((q1 | n) ^ f3))| = 0 by A1, A26, A27, A20, Th28; reconsider n1 = n as Element of NAT by ORDINAL1:def_12; 0. (TOP-REAL n) in the carrier of (TOP-REAL n) ; then f0 in REAL n by EUCLID:22; then f0 in Funcs ((Seg n1),REAL) by FINSEQ_2:93; then consider g being Function such that A29: ( f0 = g & dom g = Seg n1 & rng g c= REAL ) by FUNCT_2:def_2; A30: len f0 = len (q1 | n) by A22, A29, FINSEQ_1:def_3; len f1 = 1 by FINSEQ_1:39 .= len f3 by FINSEQ_1:39 ; then |((0. (TOP-REAL n)),p1)| + |(f1,f3)| = 0 by A28, A30, Th15; then 0 + |(f1,f3)| = 0 by EUCLID_2:33; then Sum (mlt (f1,f3)) = 0 by RVSUM_1:def_16; then Sum <*(1 * (q . (n + 1)))*> = 0 by RVSUM_1:62; hence y = f . x by A20, A25, A26, RVSUM_1:73; ::_thesis: verum end; given x being set such that A31: ( x in dom f & y = f . x ) ; ::_thesis: y in [#] (TPlane (p0,(0. (TOP-REAL (n + 1))))) reconsider p = x as Element of (TOP-REAL n) by A31; S1[p,f . p] by A17; hence y in [#] (TPlane (p0,(0. (TOP-REAL (n + 1))))) by A31; ::_thesis: verum end; then A32: rng f = [#] (TPlane (p0,(0. (TOP-REAL (n + 1))))) by FUNCT_1:def_3; for x1, x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds x1 = x2 proof let x1, x2 be set ; ::_thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 ) assume A33: ( x1 in dom f & x2 in dom f ) ; ::_thesis: ( not f . x1 = f . x2 or x1 = x2 ) assume A34: f . x1 = f . x2 ; ::_thesis: x1 = x2 reconsider p1 = x1, p2 = x2 as Element of (TOP-REAL n) by A33; ( f . p1 = p1 ^ <*0*> & f . p2 = p2 ^ <*0*> ) by A17; hence x1 = x2 by A34, FINSEQ_1:33; ::_thesis: verum end; then A35: f is one-to-one by FUNCT_1:def_4; set T1 = TOP-REAL (n + 1); A36: for p1 being Point of (TOP-REAL n) holds f . p1 is Point of (TOP-REAL (n + 1)) proof let p1 be Point of (TOP-REAL n); ::_thesis: f . p1 is Point of (TOP-REAL (n + 1)) [#] (TPlane (p0,(0. (TOP-REAL (n + 1))))) c= [#] (TOP-REAL (n + 1)) by PRE_TOPC:def_4; hence f . p1 is Point of (TOP-REAL (n + 1)) by TARSKI:def_3; ::_thesis: verum end; A37: for p1 being Point of (TOP-REAL n) for q1 being Point of (TOP-REAL (n + 1)) st q1 = f . p1 holds |.p1.| = |.q1.| proof let p1 be Point of (TOP-REAL n); ::_thesis: for q1 being Point of (TOP-REAL (n + 1)) st q1 = f . p1 holds |.p1.| = |.q1.| let q1 be Point of (TOP-REAL (n + 1)); ::_thesis: ( q1 = f . p1 implies |.p1.| = |.q1.| ) assume q1 = f . p1 ; ::_thesis: |.p1.| = |.q1.| then A38: q1 = p1 ^ <*0*> by A17; reconsider x = q1 as Element of REAL (n + 1) by EUCLID:22; A39: ( len p1 = n & rng p1 c= REAL ) by CARD_1:def_7; A40: x | n = (p1 ^ <*0*>) | (dom p1) by A38, FINSEQ_1:89 .= p1 by FINSEQ_1:21 ; A41: x . (n + 1) = 0 by A38, A39, FINSEQ_1:42; A42: |.q1.| ^2 = (|.p1.| ^2) + (0 ^2) by A40, A41, REAL_NS1:10 .= (|.p1.| ^2) + (0 * 0) by SQUARE_1:def_1 .= |.p1.| ^2 ; |.q1.| * |.q1.| >= 0 ; then A43: |.q1.| ^2 >= 0 by SQUARE_1:def_1; |.p1.| * |.p1.| >= 0 ; then |.p1.| ^2 >= 0 by SQUARE_1:def_1; hence |.p1.| = sqrt (|.q1.| ^2) by A42, SQUARE_1:def_2 .= |.q1.| by A43, SQUARE_1:def_2 ; ::_thesis: verum end; A44: for p1, p2 being Point of (TOP-REAL n) for q1, q2 being Point of (TOP-REAL (n + 1)) st q1 = f . p1 & q2 = f . p2 holds f . (p1 - p2) = q1 - q2 proof let p1, p2 be Point of (TOP-REAL n); ::_thesis: for q1, q2 being Point of (TOP-REAL (n + 1)) st q1 = f . p1 & q2 = f . p2 holds f . (p1 - p2) = q1 - q2 let q1, q2 be Point of (TOP-REAL (n + 1)); ::_thesis: ( q1 = f . p1 & q2 = f . p2 implies f . (p1 - p2) = q1 - q2 ) assume q1 = f . p1 ; ::_thesis: ( not q2 = f . p2 or f . (p1 - p2) = q1 - q2 ) then A45: q1 = p1 ^ <*0*> by A17; assume q2 = f . p2 ; ::_thesis: f . (p1 - p2) = q1 - q2 then A46: q2 = p2 ^ <*0*> by A17; A47: f . (p1 - p2) = (p1 - p2) ^ <*0*> by A17; reconsider qa = f . (p1 - p2) as Point of (TOP-REAL (n + 1)) by A36; A48: dom ((p1 - p2) ^ <*0*>) = Seg (n + 1) by FINSEQ_1:89 .= dom (q1 - q2) by FINSEQ_1:89 ; for k being Nat st k in dom (q1 - q2) holds (q1 - q2) . k = ((p1 - p2) ^ <*0*>) . k proof let k be Nat; ::_thesis: ( k in dom (q1 - q2) implies (q1 - q2) . k = ((p1 - p2) ^ <*0*>) . k ) assume k in dom (q1 - q2) ; ::_thesis: (q1 - q2) . k = ((p1 - p2) ^ <*0*>) . k then A49: k in Seg (n + 1) by FINSEQ_1:89; A50: (q1 - q2) . k = (q1 + (- q2)) . k by ALGSTR_0:def_14 .= (q1 . k) + ((- q2) . k) by A49, Th16 .= (q1 . k) + (((- 1) * q2) . k) by EUCLID:39 .= (q1 . k) + ((- 1) * (q2 . k)) by VALUED_1:6 ; A51: k in (Seg n) \/ {(n + 1)} by A49, FINSEQ_1:9; percases ( k in Seg n or k in {(n + 1)} ) by A51, XBOOLE_0:def_3; supposeA52: k in Seg n ; ::_thesis: (q1 - q2) . k = ((p1 - p2) ^ <*0*>) . k then ( k in dom p1 & k in dom p2 ) by FINSEQ_1:89; then A53: ( q1 . k = p1 . k & q2 . k = p2 . k ) by A45, A46, FINSEQ_1:def_7; k in dom (p1 - p2) by A52, FINSEQ_1:89; then ((p1 - p2) ^ <*0*>) . k = (p1 - p2) . k by FINSEQ_1:def_7 .= (p1 + (- p2)) . k by ALGSTR_0:def_14 .= (p1 . k) + ((- p2) . k) by A52, Th16 .= (p1 . k) + (((- 1) * p2) . k) by EUCLID:39 .= (p1 . k) + ((- 1) * (p2 . k)) by VALUED_1:6 ; hence (q1 - q2) . k = ((p1 - p2) ^ <*0*>) . k by A50, A53; ::_thesis: verum end; suppose k in {(n + 1)} ; ::_thesis: (q1 - q2) . k = ((p1 - p2) ^ <*0*>) . k then A54: k = n + 1 by TARSKI:def_1; ( len p1 = n & len p2 = n ) by CARD_1:def_7; then A55: ( q1 . k = 0 & q2 . k = 0 ) by A45, A46, A54, FINSEQ_1:42; len (p1 - p2) = n by CARD_1:def_7; hence (q1 - q2) . k = ((p1 - p2) ^ <*0*>) . k by A50, A55, A54, FINSEQ_1:42; ::_thesis: verum end; end; end; hence f . (p1 - p2) = q1 - q2 by A47, A48, FINSEQ_1:13; ::_thesis: verum end; A56: f .: ([#] (TOP-REAL n)) = [#] (TPlane (p0,(0. (TOP-REAL (n + 1))))) by A32, RELSET_1:22; for P being Subset of (TOP-REAL n) holds ( P is closed iff f .: P is closed ) proof let P be Subset of (TOP-REAL n); ::_thesis: ( P is closed iff f .: P is closed ) hereby ::_thesis: ( f .: P is closed implies P is closed ) assume P is closed ; ::_thesis: f .: P is closed then ([#] (TOP-REAL n)) \ P is open by PRE_TOPC:def_3; then A57: ([#] (TOP-REAL n)) \ P in the topology of (TOP-REAL n) by PRE_TOPC:def_2; set FQ = { (Ball (q,r)) where q is Point of (TOP-REAL (n + 1)), r is Real : ex p being Point of (TOP-REAL n) st ( q = f . p & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) } ; for x being set st x in { (Ball (q,r)) where q is Point of (TOP-REAL (n + 1)), r is Real : ex p being Point of (TOP-REAL n) st ( q = f . p & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) } holds x in bool ([#] (TOP-REAL (n + 1))) proof let x be set ; ::_thesis: ( x in { (Ball (q,r)) where q is Point of (TOP-REAL (n + 1)), r is Real : ex p being Point of (TOP-REAL n) st ( q = f . p & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) } implies x in bool ([#] (TOP-REAL (n + 1))) ) assume x in { (Ball (q,r)) where q is Point of (TOP-REAL (n + 1)), r is Real : ex p being Point of (TOP-REAL n) st ( q = f . p & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) } ; ::_thesis: x in bool ([#] (TOP-REAL (n + 1))) then consider q being Point of (TOP-REAL (n + 1)), r being Real such that A58: ( x = Ball (q,r) & ex p being Point of (TOP-REAL n) st ( q = f . p & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) ) ; thus x in bool ([#] (TOP-REAL (n + 1))) by A58; ::_thesis: verum end; then reconsider FQ = { (Ball (q,r)) where q is Point of (TOP-REAL (n + 1)), r is Real : ex p being Point of (TOP-REAL n) st ( q = f . p & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) } as Subset-Family of (TOP-REAL (n + 1)) by TARSKI:def_3; for Q being Subset of (TOP-REAL (n + 1)) st Q in FQ holds Q is open proof let Q be Subset of (TOP-REAL (n + 1)); ::_thesis: ( Q in FQ implies Q is open ) assume Q in FQ ; ::_thesis: Q is open then consider q being Point of (TOP-REAL (n + 1)), r being Real such that A59: ( Q = Ball (q,r) & ex p being Point of (TOP-REAL n) st ( q = f . p & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) ) ; thus Q is open by A59; ::_thesis: verum end; then A60: FQ is open by TOPS_2:def_1; set Q = union FQ; union FQ is open by A60, TOPS_2:19; then A61: union FQ in the topology of (TOP-REAL (n + 1)) by PRE_TOPC:def_2; for y being Element of (TPlane (p0,(0. (TOP-REAL (n + 1))))) holds ( y in f .: (([#] (TOP-REAL n)) \ P) iff y in (union FQ) /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) ) proof let y be Element of (TPlane (p0,(0. (TOP-REAL (n + 1))))); ::_thesis: ( y in f .: (([#] (TOP-REAL n)) \ P) iff y in (union FQ) /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) ) hereby ::_thesis: ( y in (union FQ) /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) implies y in f .: (([#] (TOP-REAL n)) \ P) ) assume y in f .: (([#] (TOP-REAL n)) \ P) ; ::_thesis: y in (union FQ) /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) then consider x being set such that A62: ( x in dom f & x in ([#] (TOP-REAL n)) \ P & y = f . x ) by FUNCT_1:def_6; reconsider p = x as Point of (TOP-REAL n) by A62; reconsider q = y as Point of (TOP-REAL (n + 1)) by A62, A36; consider r being real number such that A63: ( r > 0 & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) by A62, A57, Th24; reconsider r = r as Real by XREAL_0:def_1; A64: Ball (q,r) in FQ by A62, A63; y in Ball (q,r) by A63, JORDAN:16; then y in union FQ by A64, TARSKI:def_4; hence y in (union FQ) /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) by XBOOLE_0:def_4; ::_thesis: verum end; assume y in (union FQ) /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) ; ::_thesis: y in f .: (([#] (TOP-REAL n)) \ P) then y in union FQ by XBOOLE_0:def_4; then consider Y being set such that A65: ( y in Y & Y in FQ ) by TARSKI:def_4; consider q being Point of (TOP-REAL (n + 1)), r being Real such that A66: Y = Ball (q,r) and A67: ex p being Point of (TOP-REAL n) st ( q = f . p & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) by A65; consider p being Point of (TOP-REAL n) such that A68: ( q = f . p & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) by A67; consider x being set such that A69: ( x in dom f & y = f . x ) by A19; reconsider p1 = x as Point of (TOP-REAL n) by A69; reconsider q1 = y as Point of (TOP-REAL (n + 1)) by A69, A36; q1 in { qy where qy is Point of (TOP-REAL (n + 1)) : |.(qy - q).| < r } by A65, A66, TOPREAL9:def_1; then consider qy being Point of (TOP-REAL (n + 1)) such that A70: ( qy = q1 & |.(qy - q).| < r ) ; f . (p1 - p) = q1 - q by A69, A68, A44; then |.(p1 - p).| < r by A70, A37; then p1 in { px where px is Point of (TOP-REAL n) : |.(px - p).| < r } ; then p1 in Ball (p,r) by TOPREAL9:def_1; hence y in f .: (([#] (TOP-REAL n)) \ P) by A69, A68, FUNCT_1:def_6; ::_thesis: verum end; then A71: f .: (([#] (TOP-REAL n)) \ P) = (union FQ) /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) by SUBSET_1:3; ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) \ (f .: P) = (union FQ) /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) by A71, A35, A56, FUNCT_1:64; then ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) \ (f .: P) in the topology of (TPlane (p0,(0. (TOP-REAL (n + 1))))) by A61, PRE_TOPC:def_4; then ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) \ (f .: P) is open by PRE_TOPC:def_2; hence f .: P is closed by PRE_TOPC:def_3; ::_thesis: verum end; assume f .: P is closed ; ::_thesis: P is closed then ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) \ (f .: P) is open by PRE_TOPC:def_3; then ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) \ (f .: P) in the topology of (TPlane (p0,(0. (TOP-REAL (n + 1))))) by PRE_TOPC:def_2; then consider Q being Subset of (TOP-REAL (n + 1)) such that A72: ( Q in the topology of (TOP-REAL (n + 1)) & ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) \ (f .: P) = Q /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) ) by PRE_TOPC:def_4; for p being Point of (TOP-REAL n) st p in ([#] (TOP-REAL n)) \ P holds ex r being real number st ( r > 0 & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) proof let p be Point of (TOP-REAL n); ::_thesis: ( p in ([#] (TOP-REAL n)) \ P implies ex r being real number st ( r > 0 & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) ) assume p in ([#] (TOP-REAL n)) \ P ; ::_thesis: ex r being real number st ( r > 0 & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) then f . p in f .: (([#] (TOP-REAL n)) \ P) by A18, FUNCT_1:def_6; then A73: f . p in ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) \ (f .: P) by A56, A35, FUNCT_1:64; reconsider q = f . p as Point of (TOP-REAL (n + 1)) by A36; q in Q by A72, A73, XBOOLE_0:def_4; then consider r being real number such that A74: ( r > 0 & Ball (q,r) c= Q ) by A72, Th24; take r ; ::_thesis: ( r > 0 & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) thus r > 0 by A74; ::_thesis: Ball (p,r) c= ([#] (TOP-REAL n)) \ P for x being set st x in Ball (p,r) holds x in ([#] (TOP-REAL n)) \ P proof let x be set ; ::_thesis: ( x in Ball (p,r) implies x in ([#] (TOP-REAL n)) \ P ) assume x in Ball (p,r) ; ::_thesis: x in ([#] (TOP-REAL n)) \ P then x in { px where px is Point of (TOP-REAL n) : |.(px - p).| < r } by TOPREAL9:def_1; then consider p1 being Point of (TOP-REAL n) such that A75: ( x = p1 & |.(p1 - p).| < r ) ; reconsider q1 = f . p1 as Point of (TOP-REAL (n + 1)) by A36; f . (p1 - p) = q1 - q by A44; then |.(q1 - q).| < r by A75, A37; then q1 in { qx where qx is Point of (TOP-REAL (n + 1)) : |.(qx - q).| < r } ; then q1 in Ball (q,r) by TOPREAL9:def_1; then q1 in Q /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) by A74, XBOOLE_0:def_4; then not q1 in f .: P by A72, XBOOLE_0:def_5; then not x in P by A18, A75, FUNCT_1:def_6; hence x in ([#] (TOP-REAL n)) \ P by A75, XBOOLE_0:def_5; ::_thesis: verum end; hence Ball (p,r) c= ([#] (TOP-REAL n)) \ P by TARSKI:def_3; ::_thesis: verum end; then ([#] (TOP-REAL n)) \ P in the topology of (TOP-REAL n) by Th24; then ([#] (TOP-REAL n)) \ P is open by PRE_TOPC:def_2; hence P is closed by PRE_TOPC:def_3; ::_thesis: verum end; then f is being_homeomorphism by A18, A32, A35, TOPS_2:58; hence TOP-REAL n, TPlane (p0,(0. (TOP-REAL (n + 1)))) are_homeomorphic by T_0TOPSP:def_1; ::_thesis: verum end; theorem Th29: :: MFOLD_2:29 for n being Nat for p, q being Point of (TOP-REAL (n + 1)) st p <> 0. (TOP-REAL (n + 1)) holds TOP-REAL n, TPlane (p,q) are_homeomorphic proof let n be Nat; ::_thesis: for p, q being Point of (TOP-REAL (n + 1)) st p <> 0. (TOP-REAL (n + 1)) holds TOP-REAL n, TPlane (p,q) are_homeomorphic set T1 = TOP-REAL (n + 1); let p, q be Point of (TOP-REAL (n + 1)); ::_thesis: ( p <> 0. (TOP-REAL (n + 1)) implies TOP-REAL n, TPlane (p,q) are_homeomorphic ) assume A1: p <> 0. (TOP-REAL (n + 1)) ; ::_thesis: TOP-REAL n, TPlane (p,q) are_homeomorphic reconsider p0 = Base_FinSeq ((n + 1),(n + 1)) as Point of (TOP-REAL (n + 1)) by EUCLID:22; A2: p0 <> 0. (TOP-REAL (n + 1)) proof assume A3: p0 = 0. (TOP-REAL (n + 1)) ; ::_thesis: contradiction 0 + 1 <= n + 1 by XREAL_1:6; then |.p0.| = 1 by EUCLID_7:28; hence contradiction by A3, EUCLID_2:39; ::_thesis: verum end; A4: TOP-REAL n, TPlane (p0,(0. (TOP-REAL (n + 1)))) are_homeomorphic by Lm3; ex R being Function of (TOP-REAL (n + 1)),(TOP-REAL (n + 1)) st ( R is being_homeomorphism & R .: (Plane (p0,(0. (TOP-REAL (n + 1))))) = Plane (p,(0. (TOP-REAL (n + 1)))) ) by A1, A2, Th27; then Plane (p0,(0. (TOP-REAL (n + 1)))), Plane (p,(0. (TOP-REAL (n + 1)))) are_homeomorphic by METRIZTS:3; then TPlane (p0,(0. (TOP-REAL (n + 1)))), TPlane (p,(0. (TOP-REAL (n + 1)))) are_homeomorphic by METRIZTS:def_1; then A5: TOP-REAL n, TPlane (p,(0. (TOP-REAL (n + 1)))) are_homeomorphic by A4, BORSUK_3:3; (transl (q,(TOP-REAL (n + 1)))) .: (Plane (p,(0. (TOP-REAL (n + 1))))) = Plane (p,((0. (TOP-REAL (n + 1))) + q)) by Th25 .= Plane (p,q) by EUCLID:27 ; then Plane (p,(0. (TOP-REAL (n + 1)))), Plane (p,q) are_homeomorphic by METRIZTS:3; then (TOP-REAL (n + 1)) | (Plane (p,(0. (TOP-REAL (n + 1))))),(TOP-REAL (n + 1)) | (Plane (p,q)) are_homeomorphic by METRIZTS:def_1; hence TOP-REAL n, TPlane (p,q) are_homeomorphic by A5, BORSUK_3:3; ::_thesis: verum end; theorem :: MFOLD_2:30 for n being Nat for p, q being Point of (TOP-REAL (n + 1)) st p <> 0. (TOP-REAL (n + 1)) holds TPlane (p,q) is n -manifold proof let n be Nat; ::_thesis: for p, q being Point of (TOP-REAL (n + 1)) st p <> 0. (TOP-REAL (n + 1)) holds TPlane (p,q) is n -manifold let p, q be Point of (TOP-REAL (n + 1)); ::_thesis: ( p <> 0. (TOP-REAL (n + 1)) implies TPlane (p,q) is n -manifold ) assume p <> 0. (TOP-REAL (n + 1)) ; ::_thesis: TPlane (p,q) is n -manifold then TOP-REAL n, TPlane (p,q) are_homeomorphic by Th29; hence TPlane (p,q) is n -manifold by Th12; ::_thesis: verum end; begin definition let n be Nat; func TUnitSphere n -> TopSpace equals :: MFOLD_2:def 4 Tunit_circle (n + 1); correctness coherence Tunit_circle (n + 1) is TopSpace; ; end; :: deftheorem defines TUnitSphere MFOLD_2:def_4_:_ for n being Nat holds TUnitSphere n = Tunit_circle (n + 1); registration let n be Nat; cluster TUnitSphere n -> non empty ; correctness coherence not TUnitSphere n is empty ; ; end; 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) ; func stereographic_projection (S,p) -> Function of S,(TPlane (p,(0. (TOP-REAL n)))) means :Def5: :: MFOLD_2:def 5 for q being Point of (TOP-REAL n) st q in S holds it . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)); 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)) proof set T = TPlane (p,(0. (TOP-REAL n))); defpred S1[ set , set ] 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 set st x in [#] S holds ex y being set st ( y in [#] (TPlane (p,(0. (TOP-REAL n)))) & S1[x,y] ) proof let x be set ; ::_thesis: ( x in [#] S implies ex y being set st ( y in [#] (TPlane (p,(0. (TOP-REAL n)))) & S1[x,y] ) ) assume A3: x in [#] S ; ::_thesis: ex y being set 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)) ; ::_thesis: ( (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 + (- (0. (TOP-REAL n1)))).| = 1 by EUCLID:41; then |.(p1 + ((- 1) * (0. (TOP-REAL n1)))).| = 1 by EUCLID:39; then |.(p1 + (0. (TOP-REAL n1))).| = 1 by EUCLID:28; then |.p.| = 1 by EUCLID:27; 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 EUCLID:27; then |(p,(((1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))) + ((- 1) * (0. (TOP-REAL n)))))| = 0 by EUCLID:28; then |(p,(((1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))) + (- (0. (TOP-REAL n)))))| = 0 by EUCLID:39; then |(p,(((1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))) - (0. (TOP-REAL n))))| = 0 by EUCLID:41; 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: 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. (TOP-REAL n))))) such that A6: for x being set 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 ; ::_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)) then q in [#] S by STRUCT_0:def_5; hence f . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) by A6, A7; ::_thesis: verum end; 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 proof let f1, f2 be Function of S,(TPlane (p,(0. (TOP-REAL n)))); ::_thesis: ( ( for q being Point of (TOP-REAL n) st q in S holds f1 . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) ) & ( for q being Point of (TOP-REAL n) st q in S holds f2 . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) ) implies f1 = f2 ) assume that A8: for q being Point of (TOP-REAL n) st q in S holds f1 . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) and A9: for q being Point of (TOP-REAL n) st q in S holds f2 . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) ; ::_thesis: f1 = f2 for x being set st x in [#] S holds f1 . x = f2 . x proof let x be set ; ::_thesis: ( x in [#] S implies f1 . x = f2 . x ) assume A10: x in [#] S ; ::_thesis: f1 . x = f2 . x [#] S c= [#] (TOP-REAL n) by PRE_TOPC:def_4; then reconsider q = x as Point of (TOP-REAL n) by A10; A11: q in S by A10, STRUCT_0:def_5; thus f1 . x = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) by A11, A8 .= f2 . x by A11, A9 ; ::_thesis: verum end; hence f1 = f2 by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def5 defines stereographic_projection MFOLD_2:def_5_:_ for n being Nat for p being Point of (TOP-REAL n) for S being SubSpace of TOP-REAL n st p in Sphere ((0. (TOP-REAL n)),1) holds for b4 being Function of S,(TPlane (p,(0. (TOP-REAL n)))) holds ( b4 = stereographic_projection (S,p) iff for q being Point of (TOP-REAL n) st q in S holds b4 . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) ); theorem Th31: :: MFOLD_2:31 for n being Nat for p being Point of (TOP-REAL n) for S being SubSpace of TOP-REAL n st [#] S = (Sphere ((0. (TOP-REAL n)),1)) \ {p} & p in Sphere ((0. (TOP-REAL n)),1) holds stereographic_projection (S,p) is being_homeomorphism proof let n be Nat; ::_thesis: for p being Point of (TOP-REAL n) for S being SubSpace of TOP-REAL n st [#] S = (Sphere ((0. (TOP-REAL n)),1)) \ {p} & p in Sphere ((0. (TOP-REAL n)),1) holds stereographic_projection (S,p) is being_homeomorphism let p be Point of (TOP-REAL n); ::_thesis: for S being SubSpace of TOP-REAL n st [#] S = (Sphere ((0. (TOP-REAL n)),1)) \ {p} & p in Sphere ((0. (TOP-REAL n)),1) holds stereographic_projection (S,p) is being_homeomorphism let S be SubSpace of TOP-REAL n; ::_thesis: ( [#] S = (Sphere ((0. (TOP-REAL n)),1)) \ {p} & p in Sphere ((0. (TOP-REAL n)),1) implies stereographic_projection (S,p) is being_homeomorphism ) assume A1: [#] S = (Sphere ((0. (TOP-REAL n)),1)) \ {p} ; ::_thesis: ( not p in Sphere ((0. (TOP-REAL n)),1) or stereographic_projection (S,p) is being_homeomorphism ) assume A2: p in Sphere ((0. (TOP-REAL n)),1) ; ::_thesis: stereographic_projection (S,p) is being_homeomorphism set f = stereographic_projection (S,p); set T = TPlane (p,(0. (TOP-REAL n))); A3: dom (stereographic_projection (S,p)) = [#] S by FUNCT_2:def_1; 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 A2, TOPREAL9:9; then |.(p1 + (- (0. (TOP-REAL n1)))).| = 1 by EUCLID:41; then |.(p1 + ((- 1) * (0. (TOP-REAL n1)))).| = 1 by EUCLID:39; then |.(p1 + (0. (TOP-REAL n1))).| = 1 by EUCLID:28; then A4: |.p.| = 1 by EUCLID:27; then |(p,p)| = 1 ^2 by EUCLID_2:4; then A5: |(p,p)| = 1 * 1 by SQUARE_1:def_1; defpred S1[ set , set ] means for q being Point of (TOP-REAL n) st q = \$1 & q in TPlane (p,(0. (TOP-REAL n))) holds \$2 = (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p)); A6: for x being set st x in [#] (TPlane (p,(0. (TOP-REAL n)))) holds ex y being set st ( y in [#] S & S1[x,y] ) proof let x be set ; ::_thesis: ( x in [#] (TPlane (p,(0. (TOP-REAL n)))) implies ex y being set st ( y in [#] S & S1[x,y] ) ) assume A7: x in [#] (TPlane (p,(0. (TOP-REAL n)))) ; ::_thesis: ex y being set st ( y in [#] S & S1[x,y] ) [#] (TPlane (p,(0. (TOP-REAL n)))) c= [#] (TOP-REAL n) by PRE_TOPC:def_4; then reconsider q = x as Point of (TOP-REAL n) by A7; set y = (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p)); take (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p)) ; ::_thesis: ( (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p)) in [#] S & S1[x,(1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))] ) reconsider n1 = n as Element of NAT by ORDINAL1:def_12; reconsider p1 = p as Point of (TOP-REAL n1) ; q in Plane (p,(0. (TOP-REAL n))) by A7, PRE_TOPC:def_5; then consider x1 being Point of (TOP-REAL n) such that A8: ( x1 = q & |(p,(x1 - (0. (TOP-REAL n))))| = 0 ) ; |(p,(q + (- (0. (TOP-REAL n)))))| = 0 by A8, EUCLID:41; then |(p,(q + ((- 1) * (0. (TOP-REAL n)))))| = 0 by EUCLID:39; then |(p,(q + (0. (TOP-REAL n))))| = 0 by EUCLID:28; then A9: |(p,q)| = 0 by EUCLID:27; A10: |(q,q)| >= 0 by EUCLID_2:35; A11: not (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p)) in {p} proof assume A12: (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p)) in {p} ; ::_thesis: contradiction A13: |(((2 * q) + ((|(q,q)| - 1) * p)),p)| = (2 * |(q,p)|) + ((|(q,q)| - 1) * |(p,p)|) by EUCLID_2:25 .= (|(q,q)| - 1) * |(p,p)| by A9 ; |(((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))),p)| = (1 / (|(q,q)| + 1)) * |(((2 * q) + ((|(q,q)| - 1) * p)),p)| by EUCLID_2:19 .= ((1 / (|(q,q)| + 1)) * (|(q,q)| - 1)) * |(p,p)| by A13 ; then (|(q,q)| + 1) * 1 = (|(q,q)| + 1) * ((1 / (|(q,q)| + 1)) * (|(q,q)| - 1)) by A5, A12, TARSKI:def_1 .= ((|(q,q)| + 1) * (1 / (|(q,q)| + 1))) * (|(q,q)| - 1) .= ((|(q,q)| + 1) / (|(q,q)| + 1)) * (|(q,q)| - 1) by XCMPLX_1:99 .= 1 * (|(q,q)| - 1) by A10, XCMPLX_1:60 ; hence contradiction ; ::_thesis: verum end; reconsider y1 = (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p)) as Point of (TOP-REAL n1) ; A14: |(q,((2 * q) + ((|(q,q)| - 1) * p)))| = (2 * |(q,q)|) + ((|(q,q)| - 1) * |(p,q)|) by EUCLID_2:25 .= 2 * |(q,q)| by A9 ; A15: |(p,((2 * q) + ((|(q,q)| - 1) * p)))| = (2 * |(q,p)|) + ((|(q,q)| - 1) * |(p,p)|) by EUCLID_2:25 .= |(q,q)| - 1 by A5, A9 ; A16: |(((2 * q) + ((|(q,q)| - 1) * p)),((2 * q) + ((|(q,q)| - 1) * p)))| = (2 * (2 * |(q,q)|)) + ((|(q,q)| - 1) * |(p,((2 * q) + ((|(q,q)| - 1) * p)))|) by A14, EUCLID_2:25 .= (|(q,q)| + 1) * (|(q,q)| + 1) by A15 ; A17: |(((2 * q) + ((|(q,q)| - 1) * p)),((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))))| = (1 / (|(q,q)| + 1)) * |(((2 * q) + ((|(q,q)| - 1) * p)),((2 * q) + ((|(q,q)| - 1) * p)))| by EUCLID_2:20; |(((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))),((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))))| = (1 / (|(q,q)| + 1)) * |(((2 * q) + ((|(q,q)| - 1) * p)),((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))))| by EUCLID_2:19 .= ((1 / (|(q,q)| + 1)) * ((1 / (|(q,q)| + 1)) * (|(q,q)| + 1))) * (|(q,q)| + 1) by A16, A17 .= ((1 / (|(q,q)| + 1)) * ((|(q,q)| + 1) / (|(q,q)| + 1))) * (|(q,q)| + 1) by XCMPLX_1:99 .= ((1 / (|(q,q)| + 1)) * 1) * (|(q,q)| + 1) by A10, XCMPLX_1:60 .= (|(q,q)| + 1) / (|(q,q)| + 1) by XCMPLX_1:99 .= 1 by A10, XCMPLX_1:60 ; then |.((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))).| = 1 by EUCLID_2:5, SQUARE_1:18; then |.(((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))) + (0. (TOP-REAL n))).| = 1 by EUCLID:27; then |.(((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))) + ((- 1) * (0. (TOP-REAL n)))).| = 1 by EUCLID:28; then |.(((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))) + (- (0. (TOP-REAL n)))).| = 1 by EUCLID:39; then |.(((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))) - (0. (TOP-REAL n))).| = 1 by EUCLID:41; then y1 in Sphere ((0. (TOP-REAL n)),1) by TOPREAL9:9; hence (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p)) in [#] S by A1, A11, XBOOLE_0:def_5; ::_thesis: S1[x,(1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))] thus S1[x,(1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))] ; ::_thesis: verum end; consider g1 being Function of ([#] (TPlane (p,(0. (TOP-REAL n))))),([#] S) such that A18: for x being set st x in [#] (TPlane (p,(0. (TOP-REAL n)))) holds S1[x,g1 . x] from FUNCT_2:sch_1(A6); reconsider g = g1 as Function of (TPlane (p,(0. (TOP-REAL n)))),S ; reconsider f1 = stereographic_projection (S,p) as Function of ([#] S),([#] (TPlane (p,(0. (TOP-REAL n))))) ; |.(0. (TOP-REAL n)).| <> |.p.| by A4, EUCLID_2:39; then 0. (TOP-REAL n) <> (1 + 1) * p by EUCLID:31; then 0. (TOP-REAL n) <> (1 * p) + (1 * p) by EUCLID:33; then 0. (TOP-REAL n) <> (1 * p) + p by EUCLID:29; then 0. (TOP-REAL n) <> p + p by EUCLID:29; then p + (- p) <> p + p by EUCLID:36; then A19: not - p in {p} by TARSKI:def_1; |.(- p).| = 1 by A4, EUCLID:71; then |.((- p) + (0. (TOP-REAL n))).| = 1 by EUCLID:27; then |.((- p) + ((- 1) * (0. (TOP-REAL n)))).| = 1 by EUCLID:28; then |.((- p) + (- (0. (TOP-REAL n)))).| = 1 by EUCLID:39; then |.((- p) - (0. (TOP-REAL n))).| = 1 by EUCLID:41; then A20: - p in Sphere ((0. (TOP-REAL n1)),1) by TOPREAL9:9; then A21: [#] S <> {} by A1, A19, XBOOLE_0:def_5; A22: for y, x being set holds ( y in [#] (TPlane (p,(0. (TOP-REAL n)))) & g1 . y = x iff ( x in [#] S & f1 . x = y ) ) proof let y, x be set ; ::_thesis: ( y in [#] (TPlane (p,(0. (TOP-REAL n)))) & g1 . y = x iff ( x in [#] S & f1 . x = y ) ) hereby ::_thesis: ( x in [#] S & f1 . x = y implies ( y in [#] (TPlane (p,(0. (TOP-REAL n)))) & g1 . y = x ) ) assume A23: y in [#] (TPlane (p,(0. (TOP-REAL n)))) ; ::_thesis: ( g1 . y = x implies ( x in [#] S & f1 . x = y ) ) assume A24: g1 . y = x ; ::_thesis: ( x in [#] S & f1 . x = y ) hence A25: x in [#] S by A23, A21, FUNCT_2:5; ::_thesis: f1 . x = y [#] S c= [#] (TOP-REAL n) by PRE_TOPC:def_4; then reconsider qx = x as Point of (TOP-REAL n) by A25; [#] (TPlane (p,(0. (TOP-REAL n)))) c= [#] (TOP-REAL n) by PRE_TOPC:def_4; then reconsider qy = y as Point of (TOP-REAL n) by A23; qy in TPlane (p,(0. (TOP-REAL n))) by A23, STRUCT_0:def_5; then A26: qx = (1 / (|(qy,qy)| + 1)) * ((2 * qy) + ((|(qy,qy)| - 1) * p)) by A23, A18, A24; qx in S by A25, STRUCT_0:def_5; then A27: (stereographic_projection (S,p)) . qx = (1 / (1 - |(qx,p)|)) * (qx - (|(qx,p)| * p)) by A2, Def5; qy in Plane (p,(0. (TOP-REAL n))) by A23, PRE_TOPC:def_5; then consider y1 being Point of (TOP-REAL n) such that A28: ( y1 = qy & |(p,(y1 - (0. (TOP-REAL n))))| = 0 ) ; |(p,(qy + (- (0. (TOP-REAL n)))))| = 0 by A28, EUCLID:41; then |(p,(qy + ((- 1) * (0. (TOP-REAL n)))))| = 0 by EUCLID:39; then |(p,(qy + (0. (TOP-REAL n))))| = 0 by EUCLID:28; then A29: |(p,qy)| = 0 by EUCLID:27; A30: |(((2 * qy) + ((|(qy,qy)| - 1) * p)),p)| = (2 * |(qy,p)|) + ((|(qy,qy)| - 1) * |(p,p)|) by EUCLID_2:25 .= |(qy,qy)| - 1 by A5, A29 ; A31: |(qx,p)| = (1 / (|(qy,qy)| + 1)) * |(((2 * qy) + ((|(qy,qy)| - 1) * p)),p)| by A26, EUCLID_2:19 .= ((|(qy,qy)| - 1) / (|(qy,qy)| + 1)) * 1 by A30, XCMPLX_1:75 ; A32: |(qy,qy)| >= 0 by EUCLID_2:35; A33: 1 - |(qx,p)| = ((|(qy,qy)| + 1) / (|(qy,qy)| + 1)) - ((|(qy,qy)| - 1) / (|(qy,qy)| + 1)) by A31, A32, XCMPLX_1:60 .= ((|(qy,qy)| + 1) - (|(qy,qy)| - 1)) / (|(qy,qy)| + 1) by XCMPLX_1:120 .= 2 / (|(qy,qy)| + 1) ; A34: 1 / (1 - |(qx,p)|) = (|(qy,qy)| + 1) / 2 by A33, XCMPLX_1:57; A35: ((|(qy,qy)| + 1) / 2) * qx = (((|(qy,qy)| + 1) / 2) * (1 / (|(qy,qy)| + 1))) * ((2 * qy) + ((|(qy,qy)| - 1) * p)) by A26, EUCLID:30 .= (((|(qy,qy)| + 1) * 1) / (2 * (|(qy,qy)| + 1))) * ((2 * qy) + ((|(qy,qy)| - 1) * p)) by XCMPLX_1:76 .= (((|(qy,qy)| + 1) / (|(qy,qy)| + 1)) * (1 / 2)) * ((2 * qy) + ((|(qy,qy)| - 1) * p)) by XCMPLX_1:76 .= (1 * (1 / 2)) * ((2 * qy) + ((|(qy,qy)| - 1) * p)) by A32, XCMPLX_1:60 .= ((1 / 2) * (2 * qy)) + ((1 / 2) * ((|(qy,qy)| - 1) * p)) by EUCLID:32 .= (((1 / 2) * 2) * qy) + ((1 / 2) * ((|(qy,qy)| - 1) * p)) by EUCLID:30 .= (1 * qy) + (((1 / 2) * (|(qy,qy)| - 1)) * p) by EUCLID:30 .= qy + (((|(qy,qy)| - 1) / 2) * p) by EUCLID:29 ; A36: ((|(qy,qy)| + 1) / 2) * |(qx,p)| = ((|(qy,qy)| + 1) / (|(qy,qy)| + 1)) * ((|(qy,qy)| - 1) / 2) by A31, XCMPLX_1:85 .= 1 * ((|(qy,qy)| - 1) / 2) by A32, XCMPLX_1:60 .= (|(qy,qy)| - 1) / 2 ; thus f1 . x = (((|(qy,qy)| + 1) / 2) * qx) - (((|(qy,qy)| + 1) / 2) * (|(qx,p)| * p)) by A27, A34, EUCLID:49 .= (((|(qy,qy)| + 1) / 2) * qx) - (((|(qy,qy)| - 1) / 2) * p) by A36, EUCLID:30 .= y by A35, EUCLID:48 ; ::_thesis: verum end; assume A37: x in [#] S ; ::_thesis: ( not f1 . x = y or ( y in [#] (TPlane (p,(0. (TOP-REAL n)))) & g1 . y = x ) ) assume A38: f1 . x = y ; ::_thesis: ( y in [#] (TPlane (p,(0. (TOP-REAL n)))) & g1 . y = x ) hence A39: y in [#] (TPlane (p,(0. (TOP-REAL n)))) by A37, FUNCT_2:5; ::_thesis: g1 . y = x [#] S c= [#] (TOP-REAL n) by PRE_TOPC:def_4; then reconsider qx = x as Point of (TOP-REAL n) by A37; qx in S by A37, STRUCT_0:def_5; then A40: y = (1 / (1 - |(qx,p)|)) * (qx - (|(qx,p)| * p)) by A38, A2, Def5; then reconsider qy = y as Point of (TOP-REAL n) ; A41: qy in TPlane (p,(0. (TOP-REAL n))) by A39, STRUCT_0:def_5; A42: g1 . qy = (1 / (|(qy,qy)| + 1)) * ((2 * qy) + ((|(qy,qy)| - 1) * p)) by A41, A39, A18; reconsider qx1 = qx as Point of (TOP-REAL n1) ; qx1 in Sphere ((0. (TOP-REAL n)),1) by A37, A1, XBOOLE_0:def_5; then |.(qx1 - (0. (TOP-REAL n1))).| = 1 by TOPREAL9:9; then |.(qx1 + (- (0. (TOP-REAL n1)))).| = 1 by EUCLID:41; then |.(qx1 + ((- 1) * (0. (TOP-REAL n1)))).| = 1 by EUCLID:39; then |.(qx1 + (0. (TOP-REAL n1))).| = 1 by EUCLID:28; then |.qx.| = 1 by EUCLID:27; then |(qx,qx)| = 1 ^2 by EUCLID_2:4; then A43: |(qx,qx)| = 1 * 1 by SQUARE_1:def_1; A44: |((|(qx,p)| * p),(qx - (|(qx,p)| * p)))| = |((|(qx,p)| * p),qx)| - |((|(qx,p)| * p),(|(qx,p)| * p))| by EUCLID_2:27 .= (|(qx,p)| * |(qx,p)|) - |((|(qx,p)| * p),(|(qx,p)| * p))| by EUCLID_2:19 .= (|(qx,p)| * |(qx,p)|) - (|(qx,p)| * |(p,(|(qx,p)| * p))|) by EUCLID_2:19 .= (|(qx,p)| * |(qx,p)|) - (|(qx,p)| * (|(qx,p)| * |(p,p)|)) by EUCLID_2:20 .= 0 by A5 ; A45: |(qx,(qx - (|(qx,p)| * p)))| = |(qx,qx)| - |(qx,(|(qx,p)| * p))| by EUCLID_2:24 .= 1 - (|(qx,p)| * |(qx,p)|) by A43, EUCLID_2:20 ; A46: |((qx - (|(qx,p)| * p)),(qx - (|(qx,p)| * p)))| = |(qx,(qx - (|(qx,p)| * p)))| - |((|(qx,p)| * p),(qx - (|(qx,p)| * p)))| by EUCLID_2:24 .= (1 - (|(qx,p)| * |(qx,p)|)) + 0 by A45, A44 ; |(qx,p)| <> 1 proof assume A47: |(qx,p)| = 1 ; ::_thesis: contradiction A48: not qx in {p} by A1, A37, XBOOLE_0:def_5; |(qx,p)| - |(qx,qx)| = 0 by A43, A47; then A49: |(qx,(p - qx))| = 0 by EUCLID_2:27; |(p,p)| - |(qx,p)| = 0 by A5, A47; then A50: |((p - qx),p)| = 0 by EUCLID_2:24; |((p - qx),(p - qx))| = 0 - 0 by A49, A50, EUCLID_2:24; then p - qx = 0. (TOP-REAL n) by EUCLID_2:41; then p = qx by EUCLID:43; hence contradiction by A48, TARSKI:def_1; ::_thesis: verum end; then A51: 1 - |(qx,p)| <> 0 ; then A52: (1 - |(qx,p)|) * (1 - |(qx,p)|) <> 0 ; A53: |(qy,qy)| = (1 / (1 - |(qx,p)|)) * |((qx - (|(qx,p)| * p)),qy)| by A40, EUCLID_2:19 .= (1 / (1 - |(qx,p)|)) * ((1 / (1 - |(qx,p)|)) * |((qx - (|(qx,p)| * p)),(qx - (|(qx,p)| * p)))|) by A40, EUCLID_2:19 .= ((1 / (1 - |(qx,p)|)) * (1 / (1 - |(qx,p)|))) * (1 - (|(qx,p)| * |(qx,p)|)) by A46 .= (1 / ((1 - |(qx,p)|) * (1 - |(qx,p)|))) * (1 - (|(qx,p)| * |(qx,p)|)) by XCMPLX_1:102 .= (1 - (|(qx,p)| * |(qx,p)|)) / ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|)) by XCMPLX_1:99 ; A54: |(qy,qy)| + 1 = ((1 - (|(qx,p)| * |(qx,p)|)) / ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|))) + (((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|)) / ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|))) by A53, A52, XCMPLX_1:60 .= ((1 - (|(qx,p)| * |(qx,p)|)) + ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|))) / ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|)) by XCMPLX_1:62 .= (2 * (1 - |(qx,p)|)) / ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|)) .= 2 * ((1 - |(qx,p)|) / ((1 - |(qx,p)|) * (1 - |(qx,p)|))) by XCMPLX_1:74 .= 2 * (((1 - |(qx,p)|) / (1 - |(qx,p)|)) / (1 - |(qx,p)|)) by XCMPLX_1:78 .= 2 * (1 / (1 - |(qx,p)|)) by A51, XCMPLX_1:60 .= (2 * 1) / (1 - |(qx,p)|) by XCMPLX_1:74 ; A55: |(qy,qy)| - 1 = ((1 - (|(qx,p)| * |(qx,p)|)) / ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|))) - (((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|)) / ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|))) by A53, A52, XCMPLX_1:60 .= ((1 - (|(qx,p)| * |(qx,p)|)) - ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|))) / ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|)) by XCMPLX_1:120 .= ((2 * |(qx,p)|) * (1 - |(qx,p)|)) / ((1 - |(qx,p)|) * (1 - |(qx,p)|)) .= (2 * |(qx,p)|) * ((1 - |(qx,p)|) / ((1 - |(qx,p)|) * (1 - |(qx,p)|))) by XCMPLX_1:74 .= (2 * |(qx,p)|) * (((1 - |(qx,p)|) / (1 - |(qx,p)|)) / (1 - |(qx,p)|)) by XCMPLX_1:78 .= (2 * |(qx,p)|) * (1 / (1 - |(qx,p)|)) by A51, XCMPLX_1:60 .= ((2 * |(qx,p)|) * 1) / (1 - |(qx,p)|) by XCMPLX_1:74 ; A56: 1 / (|(qy,qy)| + 1) = (1 - |(qx,p)|) / 2 by A54, XCMPLX_1:57; A57: (|(qy,qy)| - 1) / (|(qy,qy)| + 1) = (2 * |(qx,p)|) / ((1 - |(qx,p)|) * (2 / (1 - |(qx,p)|))) by A54, A55, XCMPLX_1:78 .= (2 * |(qx,p)|) / ((2 * (1 - |(qx,p)|)) / (1 - |(qx,p)|)) by XCMPLX_1:74 .= (2 * |(qx,p)|) / (2 * ((1 - |(qx,p)|) / (1 - |(qx,p)|))) by XCMPLX_1:74 .= (2 * |(qx,p)|) / (2 * 1) by A51, XCMPLX_1:60 .= |(qx,p)| ; A58: (1 - |(qx,p)|) * qy = ((1 - |(qx,p)|) * (1 / (1 - |(qx,p)|))) * (qx - (|(qx,p)| * p)) by A40, EUCLID:30 .= (((1 - |(qx,p)|) * 1) / (1 - |(qx,p)|)) * (qx - (|(qx,p)| * p)) by XCMPLX_1:74 .= 1 * (qx - (|(qx,p)| * p)) by A51, XCMPLX_1:60 .= qx - (|(qx,p)| * p) by EUCLID:29 ; thus g1 . y = ((1 / (|(qy,qy)| + 1)) * (2 * qy)) + ((1 / (|(qy,qy)| + 1)) * ((|(qy,qy)| - 1) * p)) by A42, EUCLID:32 .= (((1 / (|(qy,qy)| + 1)) * 2) * qy) + ((1 / (|(qy,qy)| + 1)) * ((|(qy,qy)| - 1) * p)) by EUCLID:30 .= (((1 / (|(qy,qy)| + 1)) * 2) * qy) + (((1 / (|(qy,qy)| + 1)) * (|(qy,qy)| - 1)) * p) by EUCLID:30 .= ((1 - |(qx,p)|) * qy) + (((1 * (|(qy,qy)| - 1)) / (|(qy,qy)| + 1)) * p) by A56, XCMPLX_1:74 .= qx - ((|(qx,p)| * p) - (|(qx,p)| * p)) by A57, A58, EUCLID:47 .= qx - (0. (TOP-REAL n)) by EUCLID:42 .= qx + (- (0. (TOP-REAL n))) by EUCLID:41 .= qx + ((- 1) * (0. (TOP-REAL n))) by EUCLID:39 .= qx + (0. (TOP-REAL n)) by EUCLID:28 .= x by EUCLID:27 ; ::_thesis: verum end; for y being set holds ( y in [#] (TPlane (p,(0. (TOP-REAL n)))) iff ex x being set st ( x in dom (stereographic_projection (S,p)) & y = (stereographic_projection (S,p)) . x ) ) proof let y be set ; ::_thesis: ( y in [#] (TPlane (p,(0. (TOP-REAL n)))) iff ex x being set st ( x in dom (stereographic_projection (S,p)) & y = (stereographic_projection (S,p)) . x ) ) hereby ::_thesis: ( ex x being set st ( x in dom (stereographic_projection (S,p)) & y = (stereographic_projection (S,p)) . x ) implies y in [#] (TPlane (p,(0. (TOP-REAL n)))) ) assume A59: y in [#] (TPlane (p,(0. (TOP-REAL n)))) ; ::_thesis: ex x being set st ( x in dom (stereographic_projection (S,p)) & y = (stereographic_projection (S,p)) . x ) set x = g . y; take x = g . y; ::_thesis: ( x in dom (stereographic_projection (S,p)) & y = (stereographic_projection (S,p)) . x ) thus x in dom (stereographic_projection (S,p)) by A22, A3, A59; ::_thesis: y = (stereographic_projection (S,p)) . x thus y = (stereographic_projection (S,p)) . x by A59, A22; ::_thesis: verum end; given x being set such that A60: ( x in dom (stereographic_projection (S,p)) & y = (stereographic_projection (S,p)) . x ) ; ::_thesis: y in [#] (TPlane (p,(0. (TOP-REAL n)))) thus y in [#] (TPlane (p,(0. (TOP-REAL n)))) by A60, FUNCT_2:5; ::_thesis: verum end; then A61: rng (stereographic_projection (S,p)) = [#] (TPlane (p,(0. (TOP-REAL n)))) by FUNCT_1:def_3; A62: stereographic_projection (S,p) is one-to-one proof let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom (stereographic_projection (S,p)) or not x2 in dom (stereographic_projection (S,p)) or not (stereographic_projection (S,p)) . x1 = (stereographic_projection (S,p)) . x2 or x1 = x2 ) assume A63: ( x1 in dom (stereographic_projection (S,p)) & x2 in dom (stereographic_projection (S,p)) ) ; ::_thesis: ( not (stereographic_projection (S,p)) . x1 = (stereographic_projection (S,p)) . x2 or x1 = x2 ) assume A64: (stereographic_projection (S,p)) . x1 = (stereographic_projection (S,p)) . x2 ; ::_thesis: x1 = x2 ( g1 . ((stereographic_projection (S,p)) . x1) = x1 & g1 . ((stereographic_projection (S,p)) . x2) = x2 ) by A63, A22; hence x1 = x2 by A64; ::_thesis: verum end; A65: stereographic_projection (S,p) is continuous proof A66: [#] S c= [#] (TOP-REAL n) by PRE_TOPC:def_4; set f0 = InnerProduct p; consider f1 being Function of (TOP-REAL n1),R^1 such that A67: ( ( for q being Point of (TOP-REAL n) holds f1 . q = 1 ) & f1 is continuous ) by JGRAPH_2:20; consider f2 being Function of (TOP-REAL n),R^1 such that A68: ( ( for q being Point of (TOP-REAL n) for r1, r2 being real number st f1 . q = r1 & (InnerProduct p) . q = r2 holds f2 . q = r1 - r2 ) & f2 is continuous ) by A67, JGRAPH_2:21; reconsider f2 = f2 as continuous Function of (TOP-REAL n),R^1 by A68; reconsider S1 = S as non empty TopSpace by A20, A1, A19, XBOOLE_0:def_5; set f3 = f2 | S1; A69: for q being Point of (TOP-REAL n) st q in S1 holds (f2 | S1) . q = 1 - |(q,p)| proof let q be Point of (TOP-REAL n); ::_thesis: ( q in S1 implies (f2 | S1) . q = 1 - |(q,p)| ) assume q in S1 ; ::_thesis: (f2 | S1) . q = 1 - |(q,p)| then A70: q in the carrier of S1 by STRUCT_0:def_5; A71: [#] S1 c= [#] (TOP-REAL n) by PRE_TOPC:def_4; ( (InnerProduct p) . q = |(q,p)| & f1 . q = 1 ) by Def1, A67; then A72: f2 . q = 1 - |(q,p)| by A68; thus (f2 | S1) . q = (f2 | the carrier of S1) . q by A71, TMAP_1:def_3 .= 1 - |(q,p)| by A72, A70, FUNCT_1:49 ; ::_thesis: verum end; A73: for q being Point of S1 holds (f2 | S1) . q <> 0 proof let q be Point of S1; ::_thesis: (f2 | S1) . q <> 0 q in [#] S ; then reconsider qx = q as Point of (TOP-REAL n) by A66; reconsider qx1 = qx as Point of (TOP-REAL n1) ; qx1 in Sphere ((0. (TOP-REAL n)),1) by A1, XBOOLE_0:def_5; then |.(qx1 - (0. (TOP-REAL n1))).| = 1 by TOPREAL9:9; then |.(qx1 + (- (0. (TOP-REAL n1)))).| = 1 by EUCLID:41; then |.(qx1 + ((- 1) * (0. (TOP-REAL n1)))).| = 1 by EUCLID:39; then |.(qx1 + (0. (TOP-REAL n1))).| = 1 by EUCLID:28; then |.qx.| = 1 by EUCLID:27; then |(qx,qx)| = 1 ^2 by EUCLID_2:4; then A74: |(qx,qx)| = 1 * 1 by SQUARE_1:def_1; |(qx,p)| <> 1 proof assume A75: |(qx,p)| = 1 ; ::_thesis: contradiction A76: not qx in {p} by A1, XBOOLE_0:def_5; |(qx,p)| - |(qx,qx)| = 0 by A74, A75; then A77: |(qx,(p - qx))| = 0 by EUCLID_2:27; |(p,p)| - |(qx,p)| = 0 by A5, A75; then A78: |((p - qx),p)| = 0 by EUCLID_2:24; |((p - qx),(p - qx))| = 0 - 0 by A77, A78, EUCLID_2:24; then p - qx = 0. (TOP-REAL n) by EUCLID_2:41; then p = qx by EUCLID:43; hence contradiction by A76, TARSKI:def_1; ::_thesis: verum end; then A79: 1 - |(qx,p)| <> 0 ; qx in S1 by STRUCT_0:def_5; hence (f2 | S1) . q <> 0 by A69, A79; ::_thesis: verum end; then consider f4 being Function of S1,R^1 such that A80: ( ( for q being Point of S1 for r1 being real number st (f2 | S1) . q = r1 holds f4 . q = 1 / r1 ) & f4 is continuous ) by JGRAPH_2:26; consider f5 being Function of S1,(TOP-REAL n1) such that A81: ( ( for a being Point of S1 for b being Point of (TOP-REAL n) for r being real number st a = b & f4 . a = r holds f5 . b = r * b ) & f5 is continuous ) by A80, MFOLD_1:2; set f6 = (InnerProduct p) | S1; A82: for q being Point of (TOP-REAL n) st q in S1 holds ((InnerProduct p) | S1) . q = |(q,p)| proof let q be Point of (TOP-REAL n); ::_thesis: ( q in S1 implies ((InnerProduct p) | S1) . q = |(q,p)| ) assume q in S1 ; ::_thesis: ((InnerProduct p) | S1) . q = |(q,p)| then A83: q in the carrier of S1 by STRUCT_0:def_5; A84: [#] S1 c= [#] (TOP-REAL n) by PRE_TOPC:def_4; A85: (InnerProduct p) . q = |(q,p)| by Def1; thus ((InnerProduct p) | S1) . q = ((InnerProduct p) | the carrier of S1) . q by A84, TMAP_1:def_3 .= |(q,p)| by A85, A83, FUNCT_1:49 ; ::_thesis: verum end; consider f7 being Function of S1,R^1 such that A86: ( ( for q being Point of S1 for r1, r2 being real number st ((InnerProduct p) | S1) . q = r1 & (f2 | S1) . q = r2 holds f7 . q = r1 / r2 ) & f7 is continuous ) by A73, JGRAPH_2:27; reconsider p1 = - p as Point of (TOP-REAL n1) ; consider f8 being Function of S1,(TOP-REAL n1) such that A87: ( ( for r being Point of S1 holds f8 . r = (f7 . r) * p1 ) & f8 is continuous ) by A86, JGRAPH_6:9; consider f9 being Function of S,(TOP-REAL n) such that A88: ( ( for r being Point of S1 holds f9 . r = (f5 . r) + (f8 . r) ) & f9 is continuous ) by A87, A81, JGRAPH_6:12; A89: dom (stereographic_projection (S,p)) = [#] S by FUNCT_2:def_1 .= dom f9 by FUNCT_2:def_1 ; for x being set st x in dom (stereographic_projection (S,p)) holds (stereographic_projection (S,p)) . x = f9 . x proof let x be set ; ::_thesis: ( x in dom (stereographic_projection (S,p)) implies (stereographic_projection (S,p)) . x = f9 . x ) assume A90: x in dom (stereographic_projection (S,p)) ; ::_thesis: (stereographic_projection (S,p)) . x = f9 . x then x in [#] S ; then reconsider qx = x as Point of (TOP-REAL n) by A66; A91: qx in S by A90, STRUCT_0:def_5; reconsider r = qx as Point of S1 by A90; A92: (f2 | S1) . r = 1 - |(qx,p)| by A69, A91; A93: f4 . r = 1 / (1 - |(qx,p)|) by A92, A80; A94: ((InnerProduct p) | S1) . r = |(qx,p)| by A82, A91; A95: f8 . r = (f7 . r) * (- p) by A87 .= (|(qx,p)| / (1 - |(qx,p)|)) * (- p) by A92, A94, A86 ; f9 . x = (f5 . r) + (f8 . r) by A88 .= ((1 / (1 - |(qx,p)|)) * qx) + (((1 * |(qx,p)|) / (1 - |(qx,p)|)) * (- p)) by A93, A81, A95 .= ((1 / (1 - |(qx,p)|)) * qx) + (((1 / (1 - |(qx,p)|)) * |(qx,p)|) * (- p)) by XCMPLX_1:74 .= ((1 / (1 - |(qx,p)|)) * qx) + ((1 / (1 - |(qx,p)|)) * (|(qx,p)| * (- p))) by EUCLID:30 .= (1 / (1 - |(qx,p)|)) * (qx + (|(qx,p)| * (- p))) by EUCLID:32 .= (1 / (1 - |(qx,p)|)) * (qx + (- (|(qx,p)| * p))) by EUCLID:40 .= (1 / (1 - |(qx,p)|)) * (qx - (|(qx,p)| * p)) by EUCLID:41 ; hence (stereographic_projection (S,p)) . x = f9 . x by A91, A2, Def5; ::_thesis: verum end; hence stereographic_projection (S,p) is continuous by A88, A89, FUNCT_1:2, PRE_TOPC:27; ::_thesis: verum end; A96: g is continuous proof A97: for q being Point of (TOP-REAL n) st q in TPlane (p,(0. (TOP-REAL n))) holds g . q = (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p)) proof let q be Point of (TOP-REAL n); ::_thesis: ( q in TPlane (p,(0. (TOP-REAL n))) implies g . q = (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p)) ) assume A98: q in TPlane (p,(0. (TOP-REAL n))) ; ::_thesis: g . q = (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p)) then q in [#] (TPlane (p,(0. (TOP-REAL n)))) by STRUCT_0:def_5; hence g . q = (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p)) by A18, A98; ::_thesis: verum end; consider g0 being Function of (TOP-REAL n1),R^1 such that A99: ( ( for q being Point of (TOP-REAL n1) holds g0 . q = |.q.| ) & g0 is continuous ) by JORDAN2C:84; consider g1 being Function of (TOP-REAL n),R^1 such that A100: ( ( for q being Point of (TOP-REAL n) for r1 being real number st g0 . q = r1 holds g1 . q = r1 * r1 ) & g1 is continuous ) by A99, JGRAPH_2:22; consider g2 being Function of (TOP-REAL n),R^1 such that A101: ( ( for q being Point of (TOP-REAL n) for r1 being real number st g1 . q = r1 holds g2 . q = r1 + 1 ) & g2 is continuous ) by A100, JGRAPH_2:24; consider g3 being Function of (TOP-REAL n),R^1 such that A102: ( ( for q being Point of (TOP-REAL n) for r1 being real number st g1 . q = r1 holds g3 . q = r1 + (- 1) ) & g3 is continuous ) by A100, JGRAPH_2:24; consider g4 being Function of (TOP-REAL n),R^1 such that A103: ( ( for q being Point of (TOP-REAL n) holds g4 . q = 2 ) & g4 is continuous ) by JGRAPH_2:20; A104: for q being Point of (TOP-REAL n) holds g2 . q <> 0 proof let q be Point of (TOP-REAL n); ::_thesis: g2 . q <> 0 g0 . q = |.q.| by A99; then g1 . q = |.q.| * |.q.| by A100; then g2 . q = (|.q.| * |.q.|) + 1 by A101; hence g2 . q <> 0 ; ::_thesis: verum end; then consider g5 being Function of (TOP-REAL n),R^1 such that A105: ( ( for q being Point of (TOP-REAL n) for r1, r2 being real number st g4 . q = r1 & g2 . q = r2 holds g5 . q = r1 / r2 ) & g5 is continuous ) by A103, A101, JGRAPH_2:27; reconsider g6 = g5 | (TPlane (p,(0. (TOP-REAL n)))) as continuous Function of (TPlane (p,(0. (TOP-REAL n)))),R^1 by A105; consider g7 being Function of (TPlane (p,(0. (TOP-REAL n)))),(TOP-REAL n1) such that A106: ( ( for a being Point of (TPlane (p,(0. (TOP-REAL n)))) for b being Point of (TOP-REAL n) for r being real number st a = b & g6 . a = r holds g7 . b = r * b ) & g7 is continuous ) by MFOLD_1:2; consider g8 being Function of (TOP-REAL n),R^1 such that A107: ( ( for q being Point of (TOP-REAL n) for r1, r2 being real number st g3 . q = r1 & g2 . q = r2 holds g8 . q = r1 / r2 ) & g8 is continuous ) by A104, A101, A102, JGRAPH_2:27; reconsider p1 = p as Point of (TOP-REAL n1) ; reconsider g9 = g8 | (TPlane (p,(0. (TOP-REAL n)))) as continuous Function of (TPlane (p,(0. (TOP-REAL n)))),R^1 by A107; consider g10 being Function of (TPlane (p,(0. (TOP-REAL n)))),(TOP-REAL n1) such that A108: ( ( for r being Point of (TPlane (p,(0. (TOP-REAL n)))) holds g10 . r = (g9 . r) * p1 ) & g10 is continuous ) by JGRAPH_6:9; consider g11 being Function of (TPlane (p,(0. (TOP-REAL n)))),(TOP-REAL n1) such that A109: ( ( for r being Point of (TPlane (p,(0. (TOP-REAL n)))) holds g11 . r = (g7 . r) + (g10 . r) ) & g11 is continuous ) by A106, A108, JGRAPH_6:12; A110: dom g = [#] (TPlane (p,(0. (TOP-REAL n)))) by A21, FUNCT_2:def_1 .= dom g11 by FUNCT_2:def_1 ; for x being set st x in dom g holds g . x = g11 . x proof let x be set ; ::_thesis: ( x in dom g implies g . x = g11 . x ) assume A111: x in dom g ; ::_thesis: g . x = g11 . x then A112: x in [#] (TPlane (p,(0. (TOP-REAL n)))) ; [#] (TPlane (p,(0. (TOP-REAL n)))) c= [#] (TOP-REAL n) by PRE_TOPC:def_4; then reconsider qx = x as Point of (TOP-REAL n) by A112; A113: qx in TPlane (p,(0. (TOP-REAL n))) by A111, STRUCT_0:def_5; reconsider r = qx as Point of (TPlane (p,(0. (TOP-REAL n)))) by A111; A114: [#] (TPlane (p,(0. (TOP-REAL n)))) c= [#] (TOP-REAL n) by PRE_TOPC:def_4; A115: g0 . qx = |.qx.| by A99; A116: g1 . qx = |.qx.| * |.qx.| by A100, A115 .= |.qx.| ^2 by SQUARE_1:def_1 .= |(qx,qx)| by EUCLID_2:4 ; A117: g2 . qx = |(qx,qx)| + 1 by A101, A116; A118: g4 . qx = 2 by A103; A119: g6 . qx = (g5 | the carrier of (TPlane (p,(0. (TOP-REAL n))))) . qx by A114, TMAP_1:def_3 .= g5 . qx by A111, FUNCT_1:49 .= 2 / (|(qx,qx)| + 1) by A105, A118, A117 ; A120: g3 . qx = |(qx,qx)| + (- 1) by A102, A116; A121: g9 . qx = (g8 | the carrier of (TPlane (p,(0. (TOP-REAL n))))) . qx by A114, TMAP_1:def_3 .= g8 . qx by A111, FUNCT_1:49 .= (|(qx,qx)| - 1) / (|(qx,qx)| + 1) by A117, A120, A107 ; A122: g7 . r = (2 / (|(qx,qx)| + 1)) * qx by A106, A119; g11 . x = (g7 . r) + (g10 . r) by A109 .= (((1 * 2) / (|(qx,qx)| + 1)) * qx) + (((1 * (|(qx,qx)| - 1)) / (|(qx,qx)| + 1)) * p) by A121, A108, A122 .= (((1 * 2) / (|(qx,qx)| + 1)) * qx) + (((1 / (|(qx,qx)| + 1)) * (|(qx,qx)| - 1)) * p) by XCMPLX_1:74 .= (((1 / (|(qx,qx)| + 1)) * 2) * qx) + (((1 / (|(qx,qx)| + 1)) * (|(qx,qx)| - 1)) * p) by XCMPLX_1:74 .= (((1 / (|(qx,qx)| + 1)) * 2) * qx) + ((1 / (|(qx,qx)| + 1)) * ((|(qx,qx)| - 1) * p)) by EUCLID:30 .= ((1 / (|(qx,qx)| + 1)) * (2 * qx)) + ((1 / (|(qx,qx)| + 1)) * ((|(qx,qx)| - 1) * p)) by EUCLID:30 .= (1 / (|(qx,qx)| + 1)) * ((2 * qx) + ((|(qx,qx)| - 1) * p)) by EUCLID:32 ; hence g . x = g11 . x by A97, A113; ::_thesis: verum end; hence g is continuous by A109, A110, FUNCT_1:2, PRE_TOPC:27; ::_thesis: verum end; reconsider f2 = f1 as [#] (TPlane (p,(0. (TOP-REAL n)))) -valued Relation ; f2 is onto by A61, FUNCT_2:def_3; then A123: f1 " = f1 " by A62, TOPS_2:def_4; g1 = f1 " by A61, A62, A22, A21, FUNCT_2:28; hence stereographic_projection (S,p) is being_homeomorphism by A3, A61, A62, A65, A96, A123, TOPS_2:def_5; ::_thesis: verum end; registration let n be Nat; cluster TUnitSphere n -> second-countable ; correctness coherence TUnitSphere n is second-countable ; proof (TOP-REAL (n + 1)) | (Sphere ((0. (TOP-REAL (n + 1))),1)) is second-countable ; then Tcircle ((0. (TOP-REAL (n + 1))),1) is second-countable by TOPREALB:def_6; hence TUnitSphere n is second-countable by TOPREALB:def_7; ::_thesis: verum end; cluster TUnitSphere n -> n -locally_euclidean ; correctness coherence TUnitSphere n is n -locally_euclidean ; proof set M = TUnitSphere n; for p being Point of (TUnitSphere n) ex U being a_neighborhood of p st U, [#] (TOP-REAL n) are_homeomorphic proof let p be Point of (TUnitSphere n); ::_thesis: ex U being a_neighborhood of p st U, [#] (TOP-REAL n) are_homeomorphic reconsider n1 = n + 1 as Element of NAT ; A1: p in the carrier of (Tunit_circle (n + 1)) ; [#] (Tunit_circle (n + 1)) c= [#] (TOP-REAL (n + 1)) by PRE_TOPC:def_4; then reconsider p1 = p as Point of (TOP-REAL n1) by A1; A2: |.p1.| = 1 by TOPREALB:12; A3: |.(- p1).| = sqrt |((- p1),(- p1))| by EUCLID_2:37 .= sqrt |(p1,p1)| by EUCLID_2:23 .= 1 by A2, EUCLID_2:37 ; then |.((- p1) + (0. (TOP-REAL n1))).| = 1 by EUCLID:27; then |.((- p1) + ((- 1) * (0. (TOP-REAL n1)))).| = 1 by EUCLID:28; then |.((- p1) + (- (0. (TOP-REAL n1)))).| = 1 by EUCLID:39; then |.((- p1) - (0. (TOP-REAL n1))).| = 1 by EUCLID:41; then A4: - p1 in Sphere ((0. (TOP-REAL n1)),1) by TOPREAL9:9; then - p1 in [#] ((TOP-REAL n1) | (Sphere ((0. (TOP-REAL n1)),1))) by PRE_TOPC:def_5; then - p1 in the carrier of (Tcircle ((0. (TOP-REAL n1)),1)) by TOPREALB:def_6; then - p1 in the carrier of (Tunit_circle n1) by TOPREALB:def_7; then reconsider A = {(- p1)} as Subset of (TUnitSphere n) by ZFMISC_1:31; reconsider U1 = ([#] (TUnitSphere n)) \ A as Subset of (TUnitSphere n) ; |.(0. (TOP-REAL n1)).| <> |.(- p1).| by A3, EUCLID_2:39; then 0. (TOP-REAL n1) <> (1 + 1) * (- p1) by EUCLID:31; then 0. (TOP-REAL n1) <> (1 * (- p1)) + (1 * (- p1)) by EUCLID:33; then 0. (TOP-REAL n1) <> (1 * (- p1)) + (- p1) by EUCLID:29; then 0. (TOP-REAL n1) <> (- p1) + (- p1) by EUCLID:29; then (- p1) + (- (- p1)) <> (- p1) + (- p1) by EUCLID:36; then A5: not p1 in {(- p1)} by TARSKI:def_1; then p1 in U1 by XBOOLE_0:def_5; then reconsider U = U1 as a_neighborhood of p by CONNSP_2:3, FRECHET:4; take U ; ::_thesis: U, [#] (TOP-REAL n) are_homeomorphic reconsider m = n + 1 as Nat ; A6: TUnitSphere n = Tcircle ((0. (TOP-REAL m)),1) by TOPREALB:def_7 .= (TOP-REAL m) | (Sphere ((0. (TOP-REAL m)),1)) by TOPREALB:def_6 ; reconsider S = Sphere ((0. (TOP-REAL m)),1) as Subset of (TOP-REAL m) ; reconsider U11 = U1 as Subset of ((TOP-REAL m) | S) by A6; U1 c= [#] (Tunit_circle m) ; then A7: U1 c= Sphere ((0. (TOP-REAL m)),1) by A6, PRE_TOPC:def_5; then reconsider V = U11 as non empty Subset of (TOP-REAL m) by A5, XBOOLE_0:def_5, XBOOLE_1:1; (TUnitSphere n) | U = (TOP-REAL m) | V by A6, A7, PRE_TOPC:7; then reconsider U2 = (TUnitSphere n) | U as non empty SubSpace of TOP-REAL m ; reconsider p2 = - p1 as Point of (TOP-REAL m) ; p2 <> 0. (TOP-REAL m) by A3, EUCLID_2:39; then A8: TOP-REAL n, TPlane (p2,(0. (TOP-REAL m))) are_homeomorphic by Th29; A9: (TOP-REAL n) | ([#] (TOP-REAL n)) = TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) by TSEP_1:93; A10: TOP-REAL n, TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) are_homeomorphic by YELLOW14:19; [#] U2 = U by PRE_TOPC:def_5 .= the carrier of (Tcircle ((0. (TOP-REAL m)),1)) \ {p2} by TOPREALB:def_7 .= ([#] ((TOP-REAL m) | (Sphere ((0. (TOP-REAL m)),1)))) \ {p2} by TOPREALB:def_6 .= (Sphere ((0. (TOP-REAL m)),1)) \ {p2} by PRE_TOPC:def_5 ; then stereographic_projection (U2,p2) is being_homeomorphism by A4, Th31; then U2, TPlane (p2,(0. (TOP-REAL m))) are_homeomorphic by T_0TOPSP:def_1; then TOP-REAL n,U2 are_homeomorphic by A8, BORSUK_3:3; then U2, TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) are_homeomorphic by A10, BORSUK_3:3; hence U, [#] (TOP-REAL n) are_homeomorphic by A9, METRIZTS:def_1; ::_thesis: verum end; hence TUnitSphere n is n -locally_euclidean by MFOLD_1:13; ::_thesis: verum end; cluster TUnitSphere n -> n -manifold ; correctness coherence TUnitSphere n is n -manifold ; ; end;