let n1, n2 be Element of NAT ; :: thesis: ( ( h is being_of_order_0 & n1 = 0 & n2 = 0 implies n1 = n2 ) & ( not h is being_of_order_0 & n1 * h = 0_ G & n1 <> 0 & ( for m being Nat st m * h = 0_ G & m <> 0 holds
n1 <= m ) & n2 * h = 0_ G & n2 <> 0 & ( for m being Nat st m * h = 0_ G & m <> 0 holds
n2 <= m ) implies n1 = n2 ) )
thus ( h is being_of_order_0 & n1 = 0 & n2 = 0 implies n1 = n2 ) ; :: thesis: ( not h is being_of_order_0 & n1 * h = 0_ G & n1 <> 0 & ( for m being Nat st m * h = 0_ G & m <> 0 holds
n1 <= m ) & n2 * h = 0_ G & n2 <> 0 & ( for m being Nat st m * h = 0_ G & m <> 0 holds
n2 <= m ) implies n1 = n2 )
assume that
not h is being_of_order_0 and
A4: ( n1 * h = 0_ G & n1 <> 0 & ( for m being Nat st m * h = 0_ G & m <> 0 holds
n1 <= m ) & n2 * h = 0_ G & n2 <> 0 & ( for m being Nat st m * h = 0_ G & m <> 0 holds
n2 <= m ) ) ; :: thesis: n1 = n2
( n1 <= n2 & n2 <= n1 ) by A4;
hence n1 = n2 by XXREAL_0:1; :: thesis: verum