let c1, c2 be quaternion number ; :: thesis: c1 = (c1 - c2) + c2
thus (c1 - c2) + c2 = (c1 + c2) - c2 by Th5
.= c1 by Thz1 ; :: thesis: verum