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))
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:8;
A2: Im (Rotate ((a + b),r)) = ((Re (a + b)) * (sin r)) + ((Im (a + b)) * (cos r)) by Th54;
( 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 Th54;
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:8
.= 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 Th54;
( 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 Th54;
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:8
.= Re (Rotate ((a + b),r)) by A4, A1 ;
hence Rotate ((a + b),r) = (Rotate (a,r)) + (Rotate (b,r)) by A3, COMPLEX1:3; :: thesis: verum