let r be Real; :: thesis: cLoop r = CircleMap * (ExtendInt r)
for x being Point of I[01] holds (cLoop r) . x = (CircleMap * (ExtendInt r)) . x
proof
let x be Point of I[01]; :: thesis: (cLoop r) . x = (CircleMap * (ExtendInt r)) . x
A1: (ExtendInt r) . x = r * x by Def1;
thus (cLoop r) . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]| by Def4
.= |[(cos ((2 * PI) * ((ExtendInt r) . x))),(sin ((2 * PI) * ((ExtendInt r) . x)))]| by A1
.= CircleMap . ((ExtendInt r) . x) by TOPREALB:def 11
.= (CircleMap * (ExtendInt r)) . x by FUNCT_2:15 ; :: thesis: verum
end;
hence cLoop r = CircleMap * (ExtendInt r) ; :: thesis: verum