let F be non empty multLoopStr ; :: thesis: ( F is commutative & F is left_unital implies F is right_unital )
assume A1: ( F is commutative & F is left_unital ) ; :: thesis: F is right_unital
let x be Scalar of F; :: according to VECTSP_1:def 4 :: thesis: x * (1. F) = x
x * (1. F) = (1. F) * x by A1;
hence x * (1. F) = x by A1; :: thesis: verum