let s be Real; :: thesis: for f being Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2) st f is without_antipodals & 0 <= s & s <= 1 / 2 holds
H₁(f) . (s + (1 / 2)) = - (H₁(f) . s)
let f be Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2); :: thesis: ( f is without_antipodals & 0 <= s & s <= 1 / 2 implies H₁(f) . (s + (1 / 2)) = - (H₁(f) . s) )
set l = eLoop 1;
set g = Sn1->Sn f;
set t = s + (1 / 2);
assume f is without_antipodals ; :: thesis: ( not 0 <= s or not s <= 1 / 2 or H₁(f) . (s + (1 / 2)) = - (H₁(f) . s) )
then A1: Sn1->Sn f is odd by Th57;
assume A2: ( 0 <= s & s <= 1 / 2 ) ; :: thesis: H₁(f) . (s + (1 / 2)) = - (H₁(f) . s)
then A3: s + (1 / 2) in the carrier of I[01] by Lm4;
reconsider s1 = s as Point of I[01] by A2, Lm3;
A4: dom (Sn1->Sn f) = the carrier of (Tunit_circle (2 + 1)) by FUNCT_2:def 1;
A5: - ((eLoop 1) . s1) is Point of (Tcircle ((0. (TOP-REAL 3)),1)) by TOPREALC:60;
A6: (eLoop 1) . (s + (1 / 2)) = |[(cos (((2 * PI) * 1) * (s + (1 / 2)))),(sin (((2 * PI) * 1) * (s + (1 / 2)))),0]| by A3, Def7
.= |[(- (cos ((2 * PI) * s))),(sin (((2 * PI) * s) + PI)),0]| by SIN_COS:79
.= |[(- (cos ((2 * PI) * s))),(- (sin ((2 * PI) * s))),(- Q)]| by SIN_COS:79
.= - |[(cos (((2 * PI) * 1) * s)),(sin (((2 * PI) * 1) * s)),0]| by EUCLID_5:11
.= - ((eLoop 1) . s1) by Def7 ;
thus H₁(f) . (s + (1 / 2)) = (Sn1->Sn f) . ((eLoop 1) . (s + (1 / 2))) by A2, Lm4, FUNCT_2:15
.= - ((Sn1->Sn f) . ((eLoop 1) . s1)) by A1, A4, A5, A6
.= - (H₁(f) . s1) by FUNCT_2:15
.= - (H₁(f) . s) ; :: thesis: verum