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