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

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