let F be non empty multLoopStr ; :: thesis: ( F is commutative & F is left_unital implies F is well-unital )
assume A1: ( F is commutative & F is left_unital ) ; :: thesis: F is well-unital
let x be Scalar of F; :: according to VECTSP_1:def 6 :: thesis: ( x * (1. F) = x & (1. F) * x = 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 & (1. F) * x = x ) by A1; :: thesis: verum