let R be non empty multLoopStr ; :: thesis: ( R is commutative & R is right_unital implies R is left_unital )
assume that
A1: R is commutative and
A2: R is right_unital ; :: thesis: R is left_unital
let x be Element of R; :: according to VECTSP_1:def 8 :: thesis: (1. R) * x = x
thus (1. R) * x = x * (1. R) by A1, GROUP_1:def 12
.= x by A2 ; :: thesis: verum