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