%0 Journal Article
%T Mazur-Ulam Theorem
%A Artur Korni owicz
%J Formalized Mathematics
%@ 1898-9934
%D 2011
%I 
%R 10.2478/v10037-011-0020-7
%X The Mazur-Ulam theorem [15] has been formulated as two registrations: cluster bijective isometric -> midpoints-preserving Function of E, F; and cluster isometric midpoints-preserving -> Affine Function of E, F; A proof given by Jussi V is l  [23] has been formalized.
%U http://versita.metapress.com/content/xx00377237379735/?p=402fbc6153ad416ab80168a45b113833&pi=0