let n1, n2 be Nat; :: thesis: ( ( ( n1 '*' (1. R) = 0. R & n1 <> 0 & ( for m being positive Nat st m < n1 holds
m '*' (1. R) <> 0. R ) ) or ( n1 = 0 & ( for m being positive Nat holds m '*' (1. R) <> 0. R ) ) ) & ( ( n2 '*' (1. R) = 0. R & n2 <> 0 & ( for m being positive Nat st m < n2 holds
m '*' (1. R) <> 0. R ) ) or ( n2 = 0 & ( for m being positive Nat holds m '*' (1. R) <> 0. R ) ) ) implies n1 = n2 )
assume that
A5: ( ( n1 '*' (1. R) = 0. R & n1 <> 0 & ( for m being positive Nat st m < n1 holds
m '*' (1. R) <> 0. R ) ) or ( n1 = 0 & ( for m being positive Nat holds m '*' (1. R) <> 0. R ) ) ) and
A6: ( ( n2 '*' (1. R) = 0. R & n2 <> 0 & ( for m being positive Nat st m < n2 holds
m '*' (1. R) <> 0. R ) ) or ( n2 = 0 & ( for m being positive Nat holds m '*' (1. R) <> 0. R ) ) ) ; :: thesis: n1 = n2

per cases ( n1 = 0 or n1 <> 0 ) ;

suppose n1 = 0 ; :: thesis: n1 = n2

hence n1 = n2 by A5, A6; :: thesis: verum

end;

suppose n1 <> 0 ; :: thesis: n1 = n2

( not n1 < n2 & not n2 < n1 ) by A6, A5;
hence n1 = n2 by XXREAL_0:1; :: thesis: verum

end;

end;