theorem :: NIVEN:36

for L being non empty right_complementable add-associative right_zeroed addLoopStr
for z0, z1, z2, z3 being Element of L holds <%z0,z1%> - <%z2,z3%> = <%(z0 - z2),(z1 - z3)%>