per cases ( for m being positive Nat holds m '*' (1. R) <> 0. R or ex m being positive Nat st m '*' (1. R) = 0. R ) ;

suppose A1: for m being positive Nat holds m '*' (1. R) <> 0. R ; :: thesis: ex b₁ being Nat st
( ( b₁ '*' (1. R) = 0. R & b₁ <> 0 & ( for m being positive Nat st m < b₁ holds
m '*' (1. R) <> 0. R ) ) or ( b₁ = 0 & ( for m being positive Nat holds m '*' (1. R) <> 0. R ) ) )

take 0 ; :: thesis: ( ( 0 '*' (1. R) = 0. R & 0 <> 0 & ( for m being positive Nat st m < 0 holds
m '*' (1. R) <> 0. R ) ) or ( 0 = 0 & ( for m being positive Nat holds m '*' (1. R) <> 0. R ) ) )
thus ( ( 0 '*' (1. R) = 0. R & 0 <> 0 & ( for m being positive Nat st m < 0 holds
m '*' (1. R) <> 0. R ) ) or ( 0 = 0 & ( for m being positive Nat holds m '*' (1. R) <> 0. R ) ) ) by A1; :: thesis: verum

end;

suppose A2: ex m being positive Nat st m '*' (1. R) = 0. R ; :: thesis: ex b₁ being Nat st
( ( b₁ '*' (1. R) = 0. R & b₁ <> 0 & ( for m being positive Nat st m < b₁ holds
m '*' (1. R) <> 0. R ) ) or ( b₁ = 0 & ( for m being positive Nat holds m '*' (1. R) <> 0. R ) ) )

defpred S₁[ Nat] means ( $1 <> 0 & $1 '*' (1. R) = 0. R );
A3: ex k being Nat st S₁[k] by A2;
ex k being Nat st
( S₁[k] & ( for n being Nat st S₁[n] holds
k <= n ) ) from NAT_1:sch 5(A3);
then consider k being Nat such that
A4: ( S₁[k] & ( for n being Nat st S₁[n] holds
k <= n ) ) ;
take k ; :: thesis: ( ( k '*' (1. R) = 0. R & k <> 0 & ( for m being positive Nat st m < k holds
m '*' (1. R) <> 0. R ) ) or ( k = 0 & ( for m being positive Nat holds m '*' (1. R) <> 0. R ) ) )
thus ( ( k '*' (1. R) = 0. R & k <> 0 & ( for m being positive Nat st m < k holds
m '*' (1. R) <> 0. R ) ) or ( k = 0 & ( for m being positive Nat holds m '*' (1. R) <> 0. R ) ) ) by A4; :: thesis: verum

end;

end;