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