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