let n be non zero Nat; :: thesis: for f, g, B1 being Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n) st g = f (-) & B1 = f <--> g & f is without_antipodals holds
Sn1->Sn f = B1 </> ((n NormF) * B1)
let f be Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n); :: thesis: for g, B1 being Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n) st g = f (-) & B1 = f <--> g & f is without_antipodals holds
Sn1->Sn f = B1 </> ((n NormF) * B1)
let g, B1 be Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n); :: thesis: ( g = f (-) & B1 = f <--> g & f is without_antipodals implies Sn1->Sn f = B1 </> ((n NormF) * B1) )
assume that
A1: g = f (-) and
A2: B1 = f <--> g and
A3: f is without_antipodals ; :: thesis: Sn1->Sn f = B1 </> ((n NormF) * B1)
set T = Tcircle ((0. (TOP-REAL (n + 1))),1);
set B = Sn1->Sn f;
set B2 = (n NormF) * B1;
set BB = B1 </> ((n NormF) * B1);
set TC3 = Tunit_circle (n + 1);
A4: dom B1 = the carrier of (Tunit_circle (n + 1)) by FUNCT_2:def 1;
dom (n NormF) = the carrier of (TOP-REAL n) by FUNCT_2:def 1;
then rng B1 c= dom (n NormF) ;
then A5: dom ((n NormF) * B1) = dom B1 by RELAT_1:27;
A6: dom (B1 </> ((n NormF) * B1)) = (dom B1) /\ (dom ((n NormF) * B1)) by VALUED_2:71
.= the carrier of (Tunit_circle (n + 1)) by A5, FUNCT_2:def 1 ;
hence dom (Sn1->Sn f) = dom (B1 </> ((n NormF) * B1)) by FUNCT_2:def 1; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom (Sn1->Sn f) or (Sn1->Sn f) . b₁ = (B1 </> ((n NormF) * B1)) . b₁ )
let x be object ; :: thesis: ( not x in dom (Sn1->Sn f) or (Sn1->Sn f) . x = (B1 </> ((n NormF) * B1)) . x )
assume x in dom (Sn1->Sn f) ; :: thesis: (Sn1->Sn f) . x = (B1 </> ((n NormF) * B1)) . x
then reconsider x1 = x as Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) ;
reconsider y1 = - x1 as Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) by TOPREALC:60;
set p = (f . x1) - (f . y1);
A7: dom g = the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),1)) by FUNCT_2:def 1;
A8: B1 . x1 = (f . x1) - (g . x1) by A4, A2, VALUED_2:def 46
.= (f . x1) - (f . y1) by A7, A1, VALUED_2:def 34 ;
A9: ((n NormF) * B1) . x1 = (n NormF) . (B1 . x1) by FUNCT_2:15
.= |.((f . x1) - (f . y1)).| by A8, JGRAPH_4:def 1 ;
(Sn1->Sn f) . x1 = Rn->S1 ((f . x1) - (f . y1)) by Def9
.= (B1 . x1) (/) (((n NormF) * B1) . x1) by A8, A9, A3, Th56, Def8
.= (B1 . x1) (#) ((((n NormF) * B1) ") . x1) by VALUED_1:10
.= (B1 </> ((n NormF) * B1)) . x1 by A6, VALUED_2:def 43 ;
hence (Sn1->Sn f) . x = (B1 </> ((n NormF) * B1)) . x ; :: thesis: verum