let a, b be Element of 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 Th71
.= (Rotate (a,r)) - (Rotate (b,r)) by Th72 ; :: thesis: verum