let r be Real; :: thesis: eLoop r = SphereMap * (ExtendInt r)
let x be Point of I[01]; :: according to FUNCT_2:def 8 :: thesis: (eLoop r) . x = (SphereMap * (ExtendInt r)) . x
A1: (ExtendInt r) . x = r * x by TOPALG_5:def 1;
thus (eLoop r) . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| by Def7
.= |[(cos ((2 * PI) * ((ExtendInt r) . x))),(sin ((2 * PI) * ((ExtendInt r) . x))),0]| by A1
.= SphereMap . ((ExtendInt r) . x) by Def6
.= (SphereMap * (ExtendInt r)) . x by FUNCT_2:15 ; :: thesis: verum