let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for z0, z1, z2, z3 being Element of L holds <%z0,z1%> - <%z2,z3%> = <%(z0 - z2),(z1 - z3)%>
let z0, z1, z2, z3 be Element of L; :: thesis: <%z0,z1%> - <%z2,z3%> = <%(z0 - z2),(z1 - z3)%>
thus <%z0,z1%> - <%z2,z3%> = <%z0,z1%> + <%(- z2),(- z3)%> by Th31
.= <%(z0 - z2),(z1 - z3)%> by Th28 ; :: thesis: verum