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