theorem Th28: :: CAYLDICK:28

for N being non empty ConjNormAlgStr
for a1, a2, b1, b2 being Element of N st N is add-associative & N is right_zeroed & N is right_complementable holds
<%a1,b1%> - <%a2,b2%> = <%(a1 - a2),(b1 - b2)%>