:: The Definition and Basic Properties of Topological Groups :: by Artur Korni{\l}owicz :: :: Received September 7, 1998 :: Copyright (c) 1998-2012 Association of Mizar Users
uniqueness
for b1, b2 being Function of G,G st ( for x being Element of G holds b1. x = a * x ) & ( for x being Element of G holds b2. x = a * x ) holds b1= b2
uniqueness
for b1, b2 being Function of G,G st ( for x being Element of G holds b1. x = x * a ) & ( for x being Element of G holds b2. x = x * a ) holds b1= b2
:: let G be Group;
:: redefine func inverse_op G -> Function of G, G;
:: coherence;
:: end;