let SF be non empty non degenerated right_complementable almost_left_invertible right_unital well-unital distributive add-associative right_zeroed associative doubleLoopStr ; :: thesis: for x being Element of SF st x <> 0. SF holds
ex y being Element of SF st x * y = 1. SF
let x be Element of SF; :: thesis: ( x <> 0. SF implies ex y being Element of SF st x * y = 1. SF )
assume x <> 0. SF ; :: thesis: ex y being Element of SF st x * y = 1. SF
then consider y being Element of SF such that
A1: y * x = 1. SF by VECTSP_1:def 9;
take y ; :: thesis: x * y = 1. SF
y <> 0. SF by A1;
then consider z being Element of SF such that
A2: z * y = 1. SF by VECTSP_1:def 9;
z = z * (y * x) by A1
.= (1. SF) * x by A2, GROUP_1:def 3
.= x ;
hence x * y = 1. SF by A2; :: thesis: verum