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 )

thus ( v is right_invertible & v is left_invertible ) by A4; :: according to ALGSTR_0:def 29 :: thesis: verum

( 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

given w being Element of X such that A4:
( v * w = 1. X & w * v = 1. X )
; :: thesis: v is invertible
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;( 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

thus ( v is right_invertible & v is left_invertible ) by A4; :: according to ALGSTR_0:def 29 :: thesis: verum