theorem :: CIRCLED1:15

for V being RealLinearSpace
for M being Subset of V
for r being Real holds r * (Cir M) = Cir (r * M)