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)
set ab = a + b;
set rab = Rotate (a + b),r;
set ra = Rotate a,r;
set rb = Rotate b,r;
A1: ( Re (a + b) = (Re a) + (Re b) & Im (a + b) = (Im a) + (Im b) ) by COMPLEX1:19;
A2: Im (Rotate (a + b),r) = ((Re (a + b)) * (sin r)) + ((Im (a + b)) * (cos r)) by Th70;
( Im (Rotate a,r) = ((Re a) * (sin r)) + ((Im a) * (cos r)) & Im (Rotate b,r) = ((Re b) * (sin r)) + ((Im b) * (cos r)) ) by Th70;
then A3: Im ((Rotate a,r) + (Rotate b,r)) = (((Re a) * (sin r)) + ((Im a) * (cos r))) + (((Re b) * (sin r)) + ((Im b) * (cos r))) by COMPLEX1:19
.= Im (Rotate (a + b),r) by A2, A1 ;
A4: Re (Rotate (a + b),r) = ((Re (a + b)) * (cos r)) - ((Im (a + b)) * (sin r)) by Th70;
( Re (Rotate a,r) = ((Re a) * (cos r)) - ((Im a) * (sin r)) & Re (Rotate b,r) = ((Re b) * (cos r)) - ((Im b) * (sin r)) ) by Th70;
then Re ((Rotate a,r) + (Rotate b,r)) = (((Re a) * (cos r)) - ((Im a) * (sin r))) + (((Re b) * (cos r)) - ((Im b) * (sin r))) by COMPLEX1:19
.= Re (Rotate (a + b),r) by A4, A1 ;
hence Rotate (a + b),r = (Rotate a,r) + (Rotate b,r) by A3, COMPLEX1:9; :: thesis: verum