( multMagma(# REAL ,addreal #) is Group-like & multMagma(# REAL ,addreal #) is associative ) by Def3, Def4, Lm1;
hence ex b₁ being non empty multMagma st
( b₁ is strict & b₁ is Group-like & b₁ is associative ) ; :: thesis: verum