let R be Ring; :: thesis: ( Char R = 1 iff R is degenerated )

hereby :: thesis: ( R is degenerated implies Char R = 1 )

assume Char R = 1 ; :: thesis: R is degenerated
then ( 1 '*' (1. R) = 0. R & 1 <> 0 & ( for m being positive Nat st m < 1 holds
m '*' (1. R) <> 0. R ) ) by RING_3:def 5;
hence R is degenerated by RING_3:60; :: thesis: verum

end;

assume R is degenerated ; :: thesis: Char R = 1
then A: 1 '*' (1. R) = 0. R by RING_3:60;
for m being positive Nat st m < 1 holds
m '*' (1. R) <> 0. R by NAT_1:14;
hence Char R = 1 by A, RING_3:def 5; :: thesis: verum