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