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

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