let n be Nat; :: thesis: for p1, p2 being Point of () st p1 <> 0. () & p2 <> 0. () holds
ex R being Function of (),() st
( R is being_homeomorphism & R .: (Plane (p1,(0. ()))) = Plane (p2,(0. ())) )

let p1, p2 be Point of (); :: thesis: ( p1 <> 0. () & p2 <> 0. () implies ex R being Function of (),() st
( R is being_homeomorphism & R .: (Plane (p1,(0. ()))) = Plane (p2,(0. ())) ) )

assume p1 <> 0. () ; :: thesis: ( not p2 <> 0. () or ex R being Function of (),() st
( R is being_homeomorphism & R .: (Plane (p1,(0. ()))) = Plane (p2,(0. ())) ) )

then consider B1 being linearly-independent Subset of () such that
A1: ( card B1 = n - 1 & [#] (Lin B1) = Plane (p1,(0. ())) ) by Th26;
assume p2 <> 0. () ; :: thesis: ex R being Function of (),() st
( R is being_homeomorphism & R .: (Plane (p1,(0. ()))) = Plane (p2,(0. ())) )

then consider B2 being linearly-independent Subset of () such that
A2: ( card B2 = n - 1 & [#] (Lin B2) = Plane (p2,(0. ())) ) by Th26;
consider M being Matrix of n,F_Real such that
A3: ( M is invertible & () .: ([#] (Lin B1)) = [#] (Lin B2) ) by ;
reconsider M = M as invertible Matrix of n,F_Real by A3;
take Mx2Tran M ; :: thesis: ( Mx2Tran M is being_homeomorphism & () .: (Plane (p1,(0. ()))) = Plane (p2,(0. ())) )
thus ( Mx2Tran M is being_homeomorphism & () .: (Plane (p1,(0. ()))) = Plane (p2,(0. ())) ) by A1, A2, A3; :: thesis: verum