let a, b be Complex; :: thesis: for r being Real holds Rotate ((a - b),r) = (Rotate (a,r)) - (Rotate (b,r))
let r be Real; :: thesis: Rotate ((a - b),r) = (Rotate (a,r)) - (Rotate (b,r))
thus Rotate ((a - b),r) = (Rotate (a,r)) + (Rotate ((- b),r)) by Th55
.= (Rotate (a,r)) - (Rotate (b,r)) by Th56 ; :: thesis: verum