let R be non degenerated Ring; :: thesis: ( Char R = 2 iff 2 '*' (1. R) = 0. R )

now :: thesis: ( 2 '*' (1. R) = 0. R implies Char R = 2 )

assume AS: 2 '*' (1. R) = 0. R ; :: thesis: Char R = 2

now :: thesis: for m being positive Nat st m < 2 holds
m '*' (1. R) <> 0. R

let m be positive Nat; :: thesis: ( m < 2 implies m '*' (1. R) <> 0. R )
assume m < 2 ; :: thesis: m '*' (1. R) <> 0. R
then m < 1 + 1 ;
then m <= 1 by NAT_1:13;
then not not m = 0 & ... & not m = 1 ;
hence m '*' (1. R) <> 0. R by RING_3:60; :: thesis: verum

end;

hence Char R = 2 by AS, RING_3:def 5; :: thesis: verum

end;

hence ( Char R = 2 iff 2 '*' (1. R) = 0. R ) by RING_3:def 5; :: thesis: verum