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 6
.= (1. X) * y by A2, A3, GROUP_1:def 3
.= y by VECTSP_1:def 6 ;
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; :: according to ALGSTR_0:def 29 :: thesis: verum