ex c being Element of L st
for a being Element of L holds
( c *' a = c & (a + (a `)) ` = c ) by Th7;
hence ex b₁ being Element of L st
for a being Element of L holds b₁ *' a = b₁ ; :: thesis: verum