let F be non empty multLoopStr ; :: thesis: ( F is commutative & F is right_unital implies F is well-unital )
assume A2: ( F is commutative & F is right_unital ) ; :: thesis: F is well-unital
let x be Element 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 A2;
hence ( x * (1. F) = x & (1. F) * x = x ) by A2; :: thesis: verum