let f be Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2); :: thesis: for xt being Point of R^1
for L being Loop of (Sn1->Sn f) . c100a st L = H₁(f) holds
for I being Integer st S₂[f,xt,I] holds
(liftPath (L,xt)) . 1 = ((liftPath (L,xt)) . 0) + I
let xt be Point of R^1; :: thesis: for L being Loop of (Sn1->Sn f) . c100a st L = H₁(f) holds
for I being Integer st S₂[f,xt,I] holds
(liftPath (L,xt)) . 1 = ((liftPath (L,xt)) . 0) + I
let L be Loop of (Sn1->Sn f) . c100a; :: thesis: ( L = H₁(f) implies for I being Integer st S₂[f,xt,I] holds
(liftPath (L,xt)) . 1 = ((liftPath (L,xt)) . 0) + I )
assume A1: L = H₁(f) ; :: thesis: for I being Integer st S₂[f,xt,I] holds
(liftPath (L,xt)) . 1 = ((liftPath (L,xt)) . 0) + I
let I be Integer; :: thesis: ( S₂[f,xt,I] implies (liftPath (L,xt)) . 1 = ((liftPath (L,xt)) . 0) + I )
assume A2: S₂[f,xt,I] ; :: thesis: (liftPath (L,xt)) . 1 = ((liftPath (L,xt)) . 0) + I
set l = liftPath (L,xt);
(1 / 2) + (1 / 2) = 1 ;
hence (liftPath (L,xt)) . 1 = ((liftPath (L,xt)) . (Q + (1 / 2))) + (I / 2) by A1, A2
.= (((liftPath (L,xt)) . 0) + (I / 2)) + (I / 2) by A1, A2
.= ((liftPath (L,xt)) . 0) + I ;
:: thesis: verum