( H₁(R) is Abelian & H₁(R) is add-associative & H₁(R) is right_zeroed & H₁(R) is right_complementable ) by Lm4;
hence ex b₁ being non empty VectSpStr of R st
( b₁ is Abelian & b₁ is add-associative & b₁ is right_zeroed & b₁ is right_complementable & b₁ is strict ) ; :: thesis: verum