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 b1 being Nat st
( ( b1 '*' (1. R) = 0. R & b1 <> 0 & ( for m being positive Nat st m < b1 holds
m '*' (1. R) <> 0. R ) ) or ( b1 = 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 b1 being Nat st
( ( b1 '*' (1. R) = 0. R & b1 <> 0 & ( for m being positive Nat st m < b1 holds
m '*' (1. R) <> 0. R ) ) or ( b1 = 0 & ( for m being positive Nat holds m '*' (1. R) <> 0. R ) ) )
defpred S1[ Nat] means ( $1 <> 0 & $1 '*' (1. R) = 0. R );
A3: ex k being Nat st S1[k] by A2;
ex k being Nat st
( S1[k] & ( for n being Nat st S1[n] holds
k <= n ) ) from NAT_1:sch 5(A3);
then consider k being Nat such that
A4: ( S1[k] & ( for n being Nat st S1[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;