let L be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive commutative doubleLoopStr ; :: thesis: <%(0. L),(0. L),(1. L)%> = <%(0. L),(1. L)%> `^ 2
thus <%(0. L),(0. L),(1. L)%> = <%((0. L) * (0. L)),(((0. L) * (1. L)) + ((1. L) * (0. L))),((1. L) * (1. L))%>
.= <%(0. L),(1. L)%> *' <%(0. L),(1. L)%> by Th5
.= <%(0. L),(1. L)%> `^ 2 by POLYNOM5:17 ; :: thesis: verum