thus ( v is invertible implies ex w being Element of X st
( v * w = 1. X & w * v = 1. X ) ) :: thesis: ( ex w being Element of X st
( v * w = 1. X & w * v = 1. X ) implies v is invertible )

proof

assume A1: v is invertible ; :: thesis: ex w being Element of X st
( v * w = 1. X & w * v = 1. X )
then consider y being Element of X such that
A2: v * y = 1. X by ALGSTR_0:def 28;
take y ; :: thesis: ( v * y = 1. X & y * v = 1. X )
thus v * y = 1. X by A2; :: thesis: y * v = 1. X
consider x being Element of X such that
A3: x * v = 1. X by A1, ALGSTR_0:def 27;
x = x * (1. X) by VECTSP_1:def 16
.= (1. X) * y by A2, A3, GROUP_1:def 4
.= y by VECTSP_1:def 16 ;
hence y * v = 1. X by A3; :: thesis: verum

end;

given w being Element of X such that A4: ( v * w = 1. X & w * v = 1. X ) ; :: thesis: v is invertible
thus ( v is right_invertible & v is left_invertible ) by A4, ALGSTR_0:def 27, ALGSTR_0:def 28; :: according to ALGSTR_0:def 29 :: thesis: verum