let c1, c2 be Quaternion; :: thesis: c1 = (c1 - c2) + c2
thus (c1 - c2) + c2 = (c1 + c2) - c2 by Th2
.= c1 by Th7 ; :: thesis: verum