let R be Ring; :: thesis: ( R is algebraic-closed implies R is almost_right_invertible )

assume AS: R is algebraic-closed ; :: thesis: R is almost_right_invertible

let a be Element of R; :: according to ALGSTR_0:def 39 :: thesis: ( a = 0. R or a is right_invertible )

set p = <%(1. R),a%>;

assume a <> 0. R ; :: thesis: a is right_invertible

then len <%(1. R),a%> = 2 by POLYNOM5:40;

then consider b being Element of R such that

A: b is_a_root_of <%(1. R),a%> by AS, POLYNOM5:def 8, POLYNOM5:def 9;

0. R = eval (<%(1. R),a%>,b) by A, POLYNOM5:def 7

.= (1. R) + (a * b) by POLYNOM5:44 ;

then 1. R = - (a * b) by RLVECT_1:6

.= a * (- b) by VECTSP_1:8 ;

hence a is right_invertible by ALGSTR_0:def 28; :: thesis: verum

assume AS: R is algebraic-closed ; :: thesis: R is almost_right_invertible

let a be Element of R; :: according to ALGSTR_0:def 39 :: thesis: ( a = 0. R or a is right_invertible )

set p = <%(1. R),a%>;

assume a <> 0. R ; :: thesis: a is right_invertible

then len <%(1. R),a%> = 2 by POLYNOM5:40;

then consider b being Element of R such that

A: b is_a_root_of <%(1. R),a%> by AS, POLYNOM5:def 8, POLYNOM5:def 9;

0. R = eval (<%(1. R),a%>,b) by A, POLYNOM5:def 7

.= (1. R) + (a * b) by POLYNOM5:44 ;

then 1. R = - (a * b) by RLVECT_1:6

.= a * (- b) by VECTSP_1:8 ;

hence a is right_invertible by ALGSTR_0:def 28; :: thesis: verum