let N be non empty ConjNormAlgStr ; :: thesis: 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)%>
let a1, a2, b1, b2 be Element of N; :: thesis: ( N is add-associative & N is right_zeroed & N is right_complementable implies <%a1,b1%> - <%a2,b2%> = <%(a1 - a2),(b1 - b2)%> )
assume ( N is add-associative & N is right_zeroed & N is right_complementable ) ; :: thesis: <%a1,b1%> - <%a2,b2%> = <%(a1 - a2),(b1 - b2)%>
hence <%a1,b1%> - <%a2,b2%> = <%a1,b1%> + <%(- a2),(- b2)%> by Th27
.= <%(a1 - a2),(b1 - b2)%> by Def9 ;
:: thesis: verum