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 13 :: thesis: x * (1. F) = x
for F being non empty commutative multMagma
for x, y being Element of F holds x * y = y * x ;
then x * (1. F) = (1. F) * x by A1;
hence x * (1. F) = x by A1, Def19; :: thesis: verum