:: TOPALG_4 semantic presentation begin Lm1: 1 in {1,2} by TARSKI:def_2; Lm2: 2 in {1,2} by TARSKI:def_2; theorem Th1: :: TOPALG_4:1 for G, H being non empty multMagma for x being Element of (product <*G,H*>) ex g being Element of G ex h being Element of H st x = <*g,h*> proof let G, H be non empty multMagma ; ::_thesis: for x being Element of (product <*G,H*>) ex g being Element of G ex h being Element of H st x = <*g,h*> let x be Element of (product <*G,H*>); ::_thesis: ex g being Element of G ex h being Element of H st x = <*g,h*> the carrier of (product <*G,H*>) = product (Carrier <*G,H*>) by GROUP_7:def_2; then consider g being Function such that A1: x = g and A2: dom g = dom (Carrier <*G,H*>) and A3: for y being set st y in dom (Carrier <*G,H*>) holds g . y in (Carrier <*G,H*>) . y by CARD_3:def_5; A4: ex R being 1-sorted st ( R = <*G,H*> . 2 & (Carrier <*G,H*>) . 2 = the carrier of R ) by Lm2, PRALG_1:def_13; A5: dom (Carrier <*G,H*>) = {1,2} by PARTFUN1:def_2; then reconsider g = g as FinSequence by A2, FINSEQ_1:2, FINSEQ_1:def_2; g . 2 in (Carrier <*G,H*>) . 2 by A3, A5, Lm2; then reconsider h1 = g . 2 as Element of H by A4, FINSEQ_1:44; A6: ex R being 1-sorted st ( R = <*G,H*> . 1 & (Carrier <*G,H*>) . 1 = the carrier of R ) by Lm1, PRALG_1:def_13; g . 1 in (Carrier <*G,H*>) . 1 by A3, A5, Lm1; then reconsider g1 = g . 1 as Element of G by A6, FINSEQ_1:44; take g1 ; ::_thesis: ex h being Element of H st x = <*g1,h*> take h1 ; ::_thesis: x = <*g1,h1*> len g = 2 by A2, A5, FINSEQ_1:2, FINSEQ_1:def_3; hence x = <*g1,h1*> by A1, FINSEQ_1:44; ::_thesis: verum end; definition let G1, G2, H1, H2 be non empty multMagma ; let f be Function of G1,H1; let g be Function of G2,H2; func Gr2Iso (f,g) -> Function of (product <*G1,G2*>),(product <*H1,H2*>) means :Def1: :: TOPALG_4:def 1 for x being Element of (product <*G1,G2*>) ex x1 being Element of G1 ex x2 being Element of G2 st ( x = <*x1,x2*> & it . x = <*(f . x1),(g . x2)*> ); existence ex b1 being Function of (product <*G1,G2*>),(product <*H1,H2*>) st for x being Element of (product <*G1,G2*>) ex x1 being Element of G1 ex x2 being Element of G2 st ( x = <*x1,x2*> & b1 . x = <*(f . x1),(g . x2)*> ) proof defpred S1[ set , set ] means ex x1 being Element of G1 ex x2 being Element of G2 st ( \$1 = <*x1,x2*> & \$2 = <*(f . x1),(g . x2)*> ); A1: for x being Element of (product <*G1,G2*>) ex y being Element of (product <*H1,H2*>) st S1[x,y] proof let x be Element of (product <*G1,G2*>); ::_thesis: ex y being Element of (product <*H1,H2*>) st S1[x,y] consider a being Element of G1, h being Element of G2 such that A2: x = <*a,h*> by Th1; take <*(f . a),(g . h)*> ; ::_thesis: S1[x,<*(f . a),(g . h)*>] take a ; ::_thesis: ex x2 being Element of G2 st ( x = <*a,x2*> & <*(f . a),(g . h)*> = <*(f . a),(g . x2)*> ) take h ; ::_thesis: ( x = <*a,h*> & <*(f . a),(g . h)*> = <*(f . a),(g . h)*> ) thus ( x = <*a,h*> & <*(f . a),(g . h)*> = <*(f . a),(g . h)*> ) by A2; ::_thesis: verum end; ex h being Function of (product <*G1,G2*>),(product <*H1,H2*>) st for x being Element of (product <*G1,G2*>) holds S1[x,h . x] from FUNCT_2:sch_3(A1); hence ex b1 being Function of (product <*G1,G2*>),(product <*H1,H2*>) st for x being Element of (product <*G1,G2*>) ex x1 being Element of G1 ex x2 being Element of G2 st ( x = <*x1,x2*> & b1 . x = <*(f . x1),(g . x2)*> ) ; ::_thesis: verum end; uniqueness for b1, b2 being Function of (product <*G1,G2*>),(product <*H1,H2*>) st ( for x being Element of (product <*G1,G2*>) ex x1 being Element of G1 ex x2 being Element of G2 st ( x = <*x1,x2*> & b1 . x = <*(f . x1),(g . x2)*> ) ) & ( for x being Element of (product <*G1,G2*>) ex x1 being Element of G1 ex x2 being Element of G2 st ( x = <*x1,x2*> & b2 . x = <*(f . x1),(g . x2)*> ) ) holds b1 = b2 proof let F, G be Function of (product <*G1,G2*>),(product <*H1,H2*>); ::_thesis: ( ( for x being Element of (product <*G1,G2*>) ex x1 being Element of G1 ex x2 being Element of G2 st ( x = <*x1,x2*> & F . x = <*(f . x1),(g . x2)*> ) ) & ( for x being Element of (product <*G1,G2*>) ex x1 being Element of G1 ex x2 being Element of G2 st ( x = <*x1,x2*> & G . x = <*(f . x1),(g . x2)*> ) ) implies F = G ) assume that A3: for x being Element of (product <*G1,G2*>) ex x1 being Element of G1 ex x2 being Element of G2 st ( x = <*x1,x2*> & F . x = <*(f . x1),(g . x2)*> ) and A4: for x being Element of (product <*G1,G2*>) ex x1 being Element of G1 ex x2 being Element of G2 st ( x = <*x1,x2*> & G . x = <*(f . x1),(g . x2)*> ) ; ::_thesis: F = G now__::_thesis:_for_x_being_Element_of_(product_<*G1,G2*>)_holds_F_._x_=_G_._x let x be Element of (product <*G1,G2*>); ::_thesis: F . x = G . x consider x1 being Element of G1, x2 being Element of G2 such that A5: x = <*x1,x2*> and A6: F . x = <*(f . x1),(g . x2)*> by A3; consider y1 being Element of G1, y2 being Element of G2 such that A7: x = <*y1,y2*> and A8: G . x = <*(f . y1),(g . y2)*> by A4; x1 = y1 by A5, A7, FINSEQ_1:77; hence F . x = G . x by A5, A6, A7, A8, FINSEQ_1:77; ::_thesis: verum end; hence F = G by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def1 defines Gr2Iso TOPALG_4:def_1_:_ for G1, G2, H1, H2 being non empty multMagma for f being Function of G1,H1 for g being Function of G2,H2 for b7 being Function of (product <*G1,G2*>),(product <*H1,H2*>) holds ( b7 = Gr2Iso (f,g) iff for x being Element of (product <*G1,G2*>) ex x1 being Element of G1 ex x2 being Element of G2 st ( x = <*x1,x2*> & b7 . x = <*(f . x1),(g . x2)*> ) ); theorem :: TOPALG_4:2 for G1, G2, H1, H2 being non empty multMagma for f being Function of G1,H1 for g being Function of G2,H2 for x1 being Element of G1 for x2 being Element of G2 holds (Gr2Iso (f,g)) . <*x1,x2*> = <*(f . x1),(g . x2)*> proof let G1, G2, H1, H2 be non empty multMagma ; ::_thesis: for f being Function of G1,H1 for g being Function of G2,H2 for x1 being Element of G1 for x2 being Element of G2 holds (Gr2Iso (f,g)) . <*x1,x2*> = <*(f . x1),(g . x2)*> let f be Function of G1,H1; ::_thesis: for g being Function of G2,H2 for x1 being Element of G1 for x2 being Element of G2 holds (Gr2Iso (f,g)) . <*x1,x2*> = <*(f . x1),(g . x2)*> let g be Function of G2,H2; ::_thesis: for x1 being Element of G1 for x2 being Element of G2 holds (Gr2Iso (f,g)) . <*x1,x2*> = <*(f . x1),(g . x2)*> let x1 be Element of G1; ::_thesis: for x2 being Element of G2 holds (Gr2Iso (f,g)) . <*x1,x2*> = <*(f . x1),(g . x2)*> let x2 be Element of G2; ::_thesis: (Gr2Iso (f,g)) . <*x1,x2*> = <*(f . x1),(g . x2)*> consider y1 being Element of G1, y2 being Element of G2 such that A1: <*y1,y2*> = <*x1,x2*> and A2: (Gr2Iso (f,g)) . <*x1,x2*> = <*(f . y1),(g . y2)*> by Def1; x1 = y1 by A1, FINSEQ_1:77; hence (Gr2Iso (f,g)) . <*x1,x2*> = <*(f . x1),(g . x2)*> by A1, A2, FINSEQ_1:77; ::_thesis: verum end; registration let G1, G2, H1, H2 be Group; let f be Homomorphism of G1,H1; let g be Homomorphism of G2,H2; cluster Gr2Iso (f,g) -> multiplicative ; coherence Gr2Iso (f,g) is multiplicative proof set h = Gr2Iso (f,g); let a, b be Element of (product <*G1,G2*>); :: according to GROUP_6:def_6 ::_thesis: (Gr2Iso (f,g)) . (a * b) = ((Gr2Iso (f,g)) . a) * ((Gr2Iso (f,g)) . b) consider a1 being Element of G1, a2 being Element of G2 such that A1: a = <*a1,a2*> and A2: (Gr2Iso (f,g)) . a = <*(f . a1),(g . a2)*> by Def1; consider b1 being Element of G1, b2 being Element of G2 such that A3: b = <*b1,b2*> and A4: (Gr2Iso (f,g)) . b = <*(f . b1),(g . b2)*> by Def1; A5: b . 2 = b2 by A3, FINSEQ_1:44; consider r1 being Element of G1, r2 being Element of G2 such that A6: a * b = <*r1,r2*> and A7: (Gr2Iso (f,g)) . (a * b) = <*(f . r1),(g . r2)*> by Def1; ( G2 = <*G1,G2*> . 2 & a . 2 = a2 ) by A1, FINSEQ_1:44; then a2 * b2 = <*r1,r2*> . 2 by A6, A5, Lm2, GROUP_7:1; then A8: g . r2 = g . (a2 * b2) by FINSEQ_1:44 .= (g . a2) * (g . b2) by GROUP_6:def_6 ; A9: b . 1 = b1 by A3, FINSEQ_1:44; ( G1 = <*G1,G2*> . 1 & a . 1 = a1 ) by A1, FINSEQ_1:44; then a1 * b1 = <*r1,r2*> . 1 by A6, A9, Lm1, GROUP_7:1; then f . r1 = f . (a1 * b1) by FINSEQ_1:44 .= (f . a1) * (f . b1) by GROUP_6:def_6 ; hence (Gr2Iso (f,g)) . (a * b) = ((Gr2Iso (f,g)) . a) * ((Gr2Iso (f,g)) . b) by A2, A4, A7, A8, GROUP_7:29; ::_thesis: verum end; end; theorem Th3: :: TOPALG_4:3 for G1, G2, H1, H2 being non empty multMagma for f being Function of G1,H1 for g being Function of G2,H2 st f is one-to-one & g is one-to-one holds Gr2Iso (f,g) is one-to-one proof let G1, G2, H1, H2 be non empty multMagma ; ::_thesis: for f being Function of G1,H1 for g being Function of G2,H2 st f is one-to-one & g is one-to-one holds Gr2Iso (f,g) is one-to-one let f be Function of G1,H1; ::_thesis: for g being Function of G2,H2 st f is one-to-one & g is one-to-one holds Gr2Iso (f,g) is one-to-one let g be Function of G2,H2; ::_thesis: ( f is one-to-one & g is one-to-one implies Gr2Iso (f,g) is one-to-one ) assume that A1: f is one-to-one and A2: g is one-to-one ; ::_thesis: Gr2Iso (f,g) is one-to-one let a, b be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not a in proj1 (Gr2Iso (f,g)) or not b in proj1 (Gr2Iso (f,g)) or not (Gr2Iso (f,g)) . a = (Gr2Iso (f,g)) . b or a = b ) set h = Gr2Iso (f,g); assume a in dom (Gr2Iso (f,g)) ; ::_thesis: ( not b in proj1 (Gr2Iso (f,g)) or not (Gr2Iso (f,g)) . a = (Gr2Iso (f,g)) . b or a = b ) then consider a1 being Element of G1, a2 being Element of G2 such that A3: a = <*a1,a2*> and A4: (Gr2Iso (f,g)) . a = <*(f . a1),(g . a2)*> by Def1; assume b in dom (Gr2Iso (f,g)) ; ::_thesis: ( not (Gr2Iso (f,g)) . a = (Gr2Iso (f,g)) . b or a = b ) then consider b1 being Element of G1, b2 being Element of G2 such that A5: b = <*b1,b2*> and A6: (Gr2Iso (f,g)) . b = <*(f . b1),(g . b2)*> by Def1; assume A7: (Gr2Iso (f,g)) . a = (Gr2Iso (f,g)) . b ; ::_thesis: a = b then ( dom f = the carrier of G1 & f . a1 = f . b1 ) by A4, A6, FINSEQ_1:77, FUNCT_2:def_1; then A8: a1 = b1 by A1, FUNCT_1:def_4; ( dom g = the carrier of G2 & g . a2 = g . b2 ) by A4, A6, A7, FINSEQ_1:77, FUNCT_2:def_1; hence a = b by A2, A3, A5, A8, FUNCT_1:def_4; ::_thesis: verum end; theorem Th4: :: TOPALG_4:4 for G1, G2, H1, H2 being non empty multMagma for f being Function of G1,H1 for g being Function of G2,H2 st f is onto & g is onto holds Gr2Iso (f,g) is onto proof let G1, G2, H1, H2 be non empty multMagma ; ::_thesis: for f being Function of G1,H1 for g being Function of G2,H2 st f is onto & g is onto holds Gr2Iso (f,g) is onto let f be Function of G1,H1; ::_thesis: for g being Function of G2,H2 st f is onto & g is onto holds Gr2Iso (f,g) is onto let g be Function of G2,H2; ::_thesis: ( f is onto & g is onto implies Gr2Iso (f,g) is onto ) assume that A1: rng f = the carrier of H1 and A2: rng g = the carrier of H2 ; :: according to FUNCT_2:def_3 ::_thesis: Gr2Iso (f,g) is onto set h = Gr2Iso (f,g); thus rng (Gr2Iso (f,g)) c= the carrier of (product <*H1,H2*>) ; :: according to XBOOLE_0:def_10,FUNCT_2:def_3 ::_thesis: the carrier of (product <*H1,H2*>) c= rng (Gr2Iso (f,g)) let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in the carrier of (product <*H1,H2*>) or a in rng (Gr2Iso (f,g)) ) assume a in the carrier of (product <*H1,H2*>) ; ::_thesis: a in rng (Gr2Iso (f,g)) then consider x being Element of H1, y being Element of H2 such that A3: a = <*x,y*> by Th1; consider a2 being set such that A4: a2 in dom g and A5: g . a2 = y by A2, FUNCT_1:def_3; consider a1 being set such that A6: a1 in dom f and A7: f . a1 = x by A1, FUNCT_1:def_3; ( dom (Gr2Iso (f,g)) = the carrier of (product <*G1,G2*>) & ( for g being Element of G1 for h being Element of G2 holds <*g,h*> in the carrier of (product <*G1,G2*>) ) ) by FUNCT_2:def_1; then A8: <*a1,a2*> in dom (Gr2Iso (f,g)) by A6, A4; then consider k1 being Element of G1, k2 being Element of G2 such that A9: <*a1,a2*> = <*k1,k2*> and A10: (Gr2Iso (f,g)) . <*a1,a2*> = <*(f . k1),(g . k2)*> by Def1; ( a1 = k1 & a2 = k2 ) by A9, FINSEQ_1:77; hence a in rng (Gr2Iso (f,g)) by A3, A7, A5, A8, A10, FUNCT_1:def_3; ::_thesis: verum end; theorem Th5: :: TOPALG_4:5 for G1, G2, H1, H2 being Group for f being Homomorphism of G1,H1 for g being Homomorphism of G2,H2 st f is bijective & g is bijective holds Gr2Iso (f,g) is bijective proof let G1, G2, H1, H2 be Group; ::_thesis: for f being Homomorphism of G1,H1 for g being Homomorphism of G2,H2 st f is bijective & g is bijective holds Gr2Iso (f,g) is bijective let h1 be Homomorphism of G1,H1; ::_thesis: for g being Homomorphism of G2,H2 st h1 is bijective & g is bijective holds Gr2Iso (h1,g) is bijective let h2 be Homomorphism of G2,H2; ::_thesis: ( h1 is bijective & h2 is bijective implies Gr2Iso (h1,h2) is bijective ) assume that A1: h1 is bijective and A2: h2 is bijective ; ::_thesis: Gr2Iso (h1,h2) is bijective set h = Gr2Iso (h1,h2); rng h2 = the carrier of H2 by A2, GROUP_6:60; then A3: h2 is onto by FUNCT_2:def_3; rng h1 = the carrier of H1 by A1, GROUP_6:60; then h1 is onto by FUNCT_2:def_3; then Gr2Iso (h1,h2) is onto by A3, Th4; then A4: rng (Gr2Iso (h1,h2)) = the carrier of (product <*H1,H2*>) by FUNCT_2:def_3; ( h1 is one-to-one & h2 is one-to-one ) by A1, A2, GROUP_6:60; then Gr2Iso (h1,h2) is one-to-one by Th3; hence Gr2Iso (h1,h2) is bijective by A4, GROUP_6:60; ::_thesis: verum end; theorem Th6: :: TOPALG_4:6 for G1, G2, H1, H2 being Group st G1,H1 are_isomorphic & G2,H2 are_isomorphic holds product <*G1,G2*>, product <*H1,H2*> are_isomorphic proof let G1, G2, H1, H2 be Group; ::_thesis: ( G1,H1 are_isomorphic & G2,H2 are_isomorphic implies product <*G1,G2*>, product <*H1,H2*> are_isomorphic ) given h1 being Homomorphism of G1,H1 such that A1: h1 is bijective ; :: according to GROUP_6:def_11 ::_thesis: ( not G2,H2 are_isomorphic or product <*G1,G2*>, product <*H1,H2*> are_isomorphic ) given h2 being Homomorphism of G2,H2 such that A2: h2 is bijective ; :: according to GROUP_6:def_11 ::_thesis: product <*G1,G2*>, product <*H1,H2*> are_isomorphic take Gr2Iso (h1,h2) ; :: according to GROUP_6:def_11 ::_thesis: Gr2Iso (h1,h2) is bijective thus Gr2Iso (h1,h2) is bijective by A1, A2, Th5; ::_thesis: verum end; begin set I = the carrier of I[01]; reconsider j0 = 0 , j1 = 1 as Point of I[01] by BORSUK_1:def_14, BORSUK_1:def_15; theorem Th7: :: TOPALG_4:7 for f, g being Function st dom f = dom g holds pr1 <:f,g:> = f proof let f, g be Function; ::_thesis: ( dom f = dom g implies pr1 <:f,g:> = f ) assume A1: dom f = dom g ; ::_thesis: pr1 <:f,g:> = f A2: dom (pr1 <:f,g:>) = dom <:f,g:> by MCART_1:def_12; A3: for x being set st x in dom (pr1 <:f,g:>) holds (pr1 <:f,g:>) . x = f . x proof let x be set ; ::_thesis: ( x in dom (pr1 <:f,g:>) implies (pr1 <:f,g:>) . x = f . x ) assume A4: x in dom (pr1 <:f,g:>) ; ::_thesis: (pr1 <:f,g:>) . x = f . x thus (pr1 <:f,g:>) . x = (<:f,g:> . x) `1 by A2, A4, MCART_1:def_12 .= [(f . x),(g . x)] `1 by A2, A4, FUNCT_3:def_7 .= f . x ; ::_thesis: verum end; dom <:f,g:> = (dom f) /\ (dom g) by FUNCT_3:def_7 .= dom f by A1 ; hence pr1 <:f,g:> = f by A2, A3, FUNCT_1:2; ::_thesis: verum end; theorem Th8: :: TOPALG_4:8 for f, g being Function st dom f = dom g holds pr2 <:f,g:> = g proof let f, g be Function; ::_thesis: ( dom f = dom g implies pr2 <:f,g:> = g ) assume A1: dom f = dom g ; ::_thesis: pr2 <:f,g:> = g A2: dom (pr2 <:f,g:>) = dom <:f,g:> by MCART_1:def_13; A3: for x being set st x in dom (pr2 <:f,g:>) holds (pr2 <:f,g:>) . x = g . x proof let x be set ; ::_thesis: ( x in dom (pr2 <:f,g:>) implies (pr2 <:f,g:>) . x = g . x ) assume A4: x in dom (pr2 <:f,g:>) ; ::_thesis: (pr2 <:f,g:>) . x = g . x thus (pr2 <:f,g:>) . x = (<:f,g:> . x) `2 by A2, A4, MCART_1:def_13 .= [(f . x),(g . x)] `2 by A2, A4, FUNCT_3:def_7 .= g . x ; ::_thesis: verum end; dom <:f,g:> = (dom f) /\ (dom g) by FUNCT_3:def_7 .= dom g by A1 ; hence pr2 <:f,g:> = g by A2, A3, FUNCT_1:2; ::_thesis: verum end; definition let S, T, Y be non empty TopSpace; let f be Function of Y,S; let g be Function of Y,T; :: original: <: redefine func<:f,g:> -> Function of Y,[:S,T:]; coherence <:f,g:> is Function of Y,[:S,T:] proof ( dom f = the carrier of Y & dom g = the carrier of Y ) by FUNCT_2:def_1; then A1: dom <:f,g:> = the carrier of Y by FUNCT_3:50; the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by BORSUK_1:def_2; hence <:f,g:> is Function of Y,[:S,T:] by A1; ::_thesis: verum end; end; definition let S, T, Y be non empty TopSpace; let f be Function of Y,[:S,T:]; :: original: pr1 redefine func pr1 f -> Function of Y,S; coherence pr1 f is Function of Y,S proof A1: dom (pr1 f) = dom f by MCART_1:def_12; A2: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by BORSUK_1:def_2; A3: rng (pr1 f) c= the carrier of S proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (pr1 f) or y in the carrier of S ) assume y in rng (pr1 f) ; ::_thesis: y in the carrier of S then consider x being set such that A4: x in dom (pr1 f) and A5: (pr1 f) . x = y by FUNCT_1:def_3; ( (pr1 f) . x = (f . x) `1 & f . x in rng f ) by A1, A4, FUNCT_1:def_3, MCART_1:def_12; hence y in the carrier of S by A2, A5, MCART_1:10; ::_thesis: verum end; dom f = the carrier of Y by FUNCT_2:def_1; hence pr1 f is Function of Y,S by A1, A3, FUNCT_2:2; ::_thesis: verum end; :: original: pr2 redefine func pr2 f -> Function of Y,T; coherence pr2 f is Function of Y,T proof A6: dom (pr2 f) = dom f by MCART_1:def_13; A7: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by BORSUK_1:def_2; A8: rng (pr2 f) c= the carrier of T proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (pr2 f) or y in the carrier of T ) assume y in rng (pr2 f) ; ::_thesis: y in the carrier of T then consider x being set such that A9: x in dom (pr2 f) and A10: (pr2 f) . x = y by FUNCT_1:def_3; ( (pr2 f) . x = (f . x) `2 & f . x in rng f ) by A6, A9, FUNCT_1:def_3, MCART_1:def_13; hence y in the carrier of T by A7, A10, MCART_1:10; ::_thesis: verum end; dom f = the carrier of Y by FUNCT_2:def_1; hence pr2 f is Function of Y,T by A6, A8, FUNCT_2:2; ::_thesis: verum end; end; theorem Th9: :: TOPALG_4:9 for Y, S, T being non empty TopSpace for f being continuous Function of Y,[:S,T:] holds pr1 f is continuous proof let Y, S, T be non empty TopSpace; ::_thesis: for f being continuous Function of Y,[:S,T:] holds pr1 f is continuous let f be continuous Function of Y,[:S,T:]; ::_thesis: pr1 f is continuous set g = pr1 f; for p being Point of Y for V being Subset of S st (pr1 f) . p in V & V is open holds ex W being Subset of Y st ( p in W & W is open & (pr1 f) .: W c= V ) proof let p be Point of Y; ::_thesis: for V being Subset of S st (pr1 f) . p in V & V is open holds ex W being Subset of Y st ( p in W & W is open & (pr1 f) .: W c= V ) let V be Subset of S; ::_thesis: ( (pr1 f) . p in V & V is open implies ex W being Subset of Y st ( p in W & W is open & (pr1 f) .: W c= V ) ) assume that A1: (pr1 f) . p in V and A2: V is open ; ::_thesis: ex W being Subset of Y st ( p in W & W is open & (pr1 f) .: W c= V ) A3: [:V,([#] T):] is open by A2, BORSUK_1:6; the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by BORSUK_1:def_2; then consider s, t being set such that s in the carrier of S and A4: t in the carrier of T and A5: f . p = [s,t] by ZFMISC_1:def_2; A6: dom f = the carrier of Y by FUNCT_2:def_1; then (pr1 f) . p = [s,t] `1 by MCART_1:def_12, A5 .= s ; then f . p in [:V,([#] T):] by A1, A4, A5, ZFMISC_1:87; then consider W being Subset of Y such that A7: ( p in W & W is open ) and A8: f .: W c= [:V,([#] T):] by A3, JGRAPH_2:10; take W ; ::_thesis: ( p in W & W is open & (pr1 f) .: W c= V ) thus ( p in W & W is open ) by A7; ::_thesis: (pr1 f) .: W c= V let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (pr1 f) .: W or y in V ) assume y in (pr1 f) .: W ; ::_thesis: y in V then consider x being Point of Y such that A9: x in W and A10: y = (pr1 f) . x by FUNCT_2:65; A11: (pr1 f) . x = (f . x) `1 by A6, MCART_1:def_12; f . x in f .: W by A6, A9, FUNCT_1:def_6; hence y in V by A8, A10, A11, MCART_1:10; ::_thesis: verum end; hence pr1 f is continuous by JGRAPH_2:10; ::_thesis: verum end; theorem Th10: :: TOPALG_4:10 for Y, S, T being non empty TopSpace for f being continuous Function of Y,[:S,T:] holds pr2 f is continuous proof let Y, S, T be non empty TopSpace; ::_thesis: for f being continuous Function of Y,[:S,T:] holds pr2 f is continuous let f be continuous Function of Y,[:S,T:]; ::_thesis: pr2 f is continuous set g = pr2 f; for p being Point of Y for V being Subset of T st (pr2 f) . p in V & V is open holds ex W being Subset of Y st ( p in W & W is open & (pr2 f) .: W c= V ) proof let p be Point of Y; ::_thesis: for V being Subset of T st (pr2 f) . p in V & V is open holds ex W being Subset of Y st ( p in W & W is open & (pr2 f) .: W c= V ) let V be Subset of T; ::_thesis: ( (pr2 f) . p in V & V is open implies ex W being Subset of Y st ( p in W & W is open & (pr2 f) .: W c= V ) ) assume that A1: (pr2 f) . p in V and A2: V is open ; ::_thesis: ex W being Subset of Y st ( p in W & W is open & (pr2 f) .: W c= V ) A3: [:([#] S),V:] is open by A2, BORSUK_1:6; the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by BORSUK_1:def_2; then consider s, t being set such that A4: s in the carrier of S and t in the carrier of T and A5: f . p = [s,t] by ZFMISC_1:def_2; A6: dom f = the carrier of Y by FUNCT_2:def_1; then (pr2 f) . p = [s,t] `2 by MCART_1:def_13, A5 .= t ; then f . p in [:([#] S),V:] by A1, A4, A5, ZFMISC_1:87; then consider W being Subset of Y such that A7: ( p in W & W is open ) and A8: f .: W c= [:([#] S),V:] by A3, JGRAPH_2:10; take W ; ::_thesis: ( p in W & W is open & (pr2 f) .: W c= V ) thus ( p in W & W is open ) by A7; ::_thesis: (pr2 f) .: W c= V let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (pr2 f) .: W or y in V ) assume y in (pr2 f) .: W ; ::_thesis: y in V then consider x being Point of Y such that A9: x in W and A10: y = (pr2 f) . x by FUNCT_2:65; A11: (pr2 f) . x = (f . x) `2 by A6, MCART_1:def_13; f . x in f .: W by A6, A9, FUNCT_1:def_6; hence y in V by A8, A10, A11, MCART_1:10; ::_thesis: verum end; hence pr2 f is continuous by JGRAPH_2:10; ::_thesis: verum end; theorem Th11: :: TOPALG_4:11 for S, T being non empty TopSpace for s1, s2 being Point of S for t1, t2 being Point of T st [s1,t1],[s2,t2] are_connected holds s1,s2 are_connected proof let S, T be non empty TopSpace; ::_thesis: for s1, s2 being Point of S for t1, t2 being Point of T st [s1,t1],[s2,t2] are_connected holds s1,s2 are_connected let s1, s2 be Point of S; ::_thesis: for t1, t2 being Point of T st [s1,t1],[s2,t2] are_connected holds s1,s2 are_connected let t1, t2 be Point of T; ::_thesis: ( [s1,t1],[s2,t2] are_connected implies s1,s2 are_connected ) given L being Function of I[01],[:S,T:] such that A1: L is continuous and A2: L . 0 = [s1,t1] and A3: L . 1 = [s2,t2] ; :: according to BORSUK_2:def_1 ::_thesis: s1,s2 are_connected take f = pr1 L; :: according to BORSUK_2:def_1 ::_thesis: ( f is continuous & f . 0 = s1 & f . 1 = s2 ) thus f is continuous by A1, Th9; ::_thesis: ( f . 0 = s1 & f . 1 = s2 ) A4: ( dom f = the carrier of I[01] & dom f = dom L ) by FUNCT_2:def_1, MCART_1:def_12; then j0 in dom L ; hence f . 0 = [s1,t1] `1 by MCART_1:def_12, A2 .= s1 ; ::_thesis: f . 1 = s2 j1 in dom L by A4; hence f . 1 = [s2,t2] `1 by MCART_1:def_12, A3 .= s2 ; ::_thesis: verum end; theorem Th12: :: TOPALG_4:12 for S, T being non empty TopSpace for s1, s2 being Point of S for t1, t2 being Point of T st [s1,t1],[s2,t2] are_connected holds t1,t2 are_connected proof let S, T be non empty TopSpace; ::_thesis: for s1, s2 being Point of S for t1, t2 being Point of T st [s1,t1],[s2,t2] are_connected holds t1,t2 are_connected let s1, s2 be Point of S; ::_thesis: for t1, t2 being Point of T st [s1,t1],[s2,t2] are_connected holds t1,t2 are_connected let t1, t2 be Point of T; ::_thesis: ( [s1,t1],[s2,t2] are_connected implies t1,t2 are_connected ) given L being Function of I[01],[:S,T:] such that A1: L is continuous and A2: L . 0 = [s1,t1] and A3: L . 1 = [s2,t2] ; :: according to BORSUK_2:def_1 ::_thesis: t1,t2 are_connected take f = pr2 L; :: according to BORSUK_2:def_1 ::_thesis: ( f is continuous & f . 0 = t1 & f . 1 = t2 ) thus f is continuous by A1, Th10; ::_thesis: ( f . 0 = t1 & f . 1 = t2 ) A4: ( dom f = the carrier of I[01] & dom f = dom L ) by FUNCT_2:def_1, MCART_1:def_13; then j0 in dom L ; hence f . 0 = [s1,t1] `2 by MCART_1:def_13, A2 .= t1 ; ::_thesis: f . 1 = t2 j1 in dom L by A4; hence f . 1 = [s2,t2] `2 by MCART_1:def_13, A3 .= t2 ; ::_thesis: verum end; theorem Th13: :: TOPALG_4:13 for S, T being non empty TopSpace for s1, s2 being Point of S for t1, t2 being Point of T st [s1,t1],[s2,t2] are_connected holds for L being Path of [s1,t1],[s2,t2] holds pr1 L is Path of s1,s2 proof let S, T be non empty TopSpace; ::_thesis: for s1, s2 being Point of S for t1, t2 being Point of T st [s1,t1],[s2,t2] are_connected holds for L being Path of [s1,t1],[s2,t2] holds pr1 L is Path of s1,s2 let s1, s2 be Point of S; ::_thesis: for t1, t2 being Point of T st [s1,t1],[s2,t2] are_connected holds for L being Path of [s1,t1],[s2,t2] holds pr1 L is Path of s1,s2 let t1, t2 be Point of T; ::_thesis: ( [s1,t1],[s2,t2] are_connected implies for L being Path of [s1,t1],[s2,t2] holds pr1 L is Path of s1,s2 ) assume A1: [s1,t1],[s2,t2] are_connected ; ::_thesis: for L being Path of [s1,t1],[s2,t2] holds pr1 L is Path of s1,s2 let L be Path of [s1,t1],[s2,t2]; ::_thesis: pr1 L is Path of s1,s2 set f = pr1 L; A2: ( dom (pr1 L) = the carrier of I[01] & dom (pr1 L) = dom L ) by FUNCT_2:def_1, MCART_1:def_12; then j0 in dom L ; then A3: (pr1 L) . 0 = (L . 0) `1 by MCART_1:def_12 .= [s1,t1] `1 by A1, BORSUK_2:def_2 .= s1 ; j1 in dom L by A2; then A4: (pr1 L) . 1 = (L . 1) `1 by MCART_1:def_12 .= [s2,t2] `1 by A1, BORSUK_2:def_2 .= s2 ; L is continuous by A1, BORSUK_2:def_2; then A5: pr1 L is continuous by Th9; then s1,s2 are_connected by A3, A4, BORSUK_2:def_1; hence pr1 L is Path of s1,s2 by A5, A3, A4, BORSUK_2:def_2; ::_thesis: verum end; theorem Th14: :: TOPALG_4:14 for S, T being non empty TopSpace for s1, s2 being Point of S for t1, t2 being Point of T st [s1,t1],[s2,t2] are_connected holds for L being Path of [s1,t1],[s2,t2] holds pr2 L is Path of t1,t2 proof let S, T be non empty TopSpace; ::_thesis: for s1, s2 being Point of S for t1, t2 being Point of T st [s1,t1],[s2,t2] are_connected holds for L being Path of [s1,t1],[s2,t2] holds pr2 L is Path of t1,t2 let s1, s2 be Point of S; ::_thesis: for t1, t2 being Point of T st [s1,t1],[s2,t2] are_connected holds for L being Path of [s1,t1],[s2,t2] holds pr2 L is Path of t1,t2 let t1, t2 be Point of T; ::_thesis: ( [s1,t1],[s2,t2] are_connected implies for L being Path of [s1,t1],[s2,t2] holds pr2 L is Path of t1,t2 ) assume A1: [s1,t1],[s2,t2] are_connected ; ::_thesis: for L being Path of [s1,t1],[s2,t2] holds pr2 L is Path of t1,t2 let L be Path of [s1,t1],[s2,t2]; ::_thesis: pr2 L is Path of t1,t2 set f = pr2 L; A2: ( dom (pr2 L) = the carrier of I[01] & dom (pr2 L) = dom L ) by FUNCT_2:def_1, MCART_1:def_13; then j0 in dom L ; then A3: (pr2 L) . 0 = (L . 0) `2 by MCART_1:def_13 .= [s1,t1] `2 by A1, BORSUK_2:def_2 .= t1 ; j1 in dom L by A2; then A4: (pr2 L) . 1 = (L . 1) `2 by MCART_1:def_13 .= [s2,t2] `2 by A1, BORSUK_2:def_2 .= t2 ; L is continuous by A1, BORSUK_2:def_2; then A5: pr2 L is continuous by Th10; then t1,t2 are_connected by A3, A4, BORSUK_2:def_1; hence pr2 L is Path of t1,t2 by A5, A3, A4, BORSUK_2:def_2; ::_thesis: verum end; theorem Th15: :: TOPALG_4:15 for S, T being non empty TopSpace for s1, s2 being Point of S for t1, t2 being Point of T st s1,s2 are_connected & t1,t2 are_connected holds [s1,t1],[s2,t2] are_connected proof let S, T be non empty TopSpace; ::_thesis: for s1, s2 being Point of S for t1, t2 being Point of T st s1,s2 are_connected & t1,t2 are_connected holds [s1,t1],[s2,t2] are_connected let s1, s2 be Point of S; ::_thesis: for t1, t2 being Point of T st s1,s2 are_connected & t1,t2 are_connected holds [s1,t1],[s2,t2] are_connected let t1, t2 be Point of T; ::_thesis: ( s1,s2 are_connected & t1,t2 are_connected implies [s1,t1],[s2,t2] are_connected ) given f being Function of I[01],S such that A1: f is continuous and A2: f . 0 = s1 and A3: f . 1 = s2 ; :: according to BORSUK_2:def_1 ::_thesis: ( not t1,t2 are_connected or [s1,t1],[s2,t2] are_connected ) given g being Function of I[01],T such that A4: g is continuous and A5: g . 0 = t1 and A6: g . 1 = t2 ; :: according to BORSUK_2:def_1 ::_thesis: [s1,t1],[s2,t2] are_connected take <:f,g:> ; :: according to BORSUK_2:def_1 ::_thesis: ( <:f,g:> is continuous & <:f,g:> . 0 = [s1,t1] & <:f,g:> . 1 = [s2,t2] ) thus <:f,g:> is continuous by A1, A4, YELLOW12:41; ::_thesis: ( <:f,g:> . 0 = [s1,t1] & <:f,g:> . 1 = [s2,t2] ) A7: ( dom f = the carrier of I[01] & dom g = the carrier of I[01] ) by FUNCT_2:def_1; hence <:f,g:> . 0 = [(f . j0),(g . j0)] by FUNCT_3:49 .= [s1,t1] by A2, A5 ; ::_thesis: <:f,g:> . 1 = [s2,t2] thus <:f,g:> . 1 = [(f . j1),(g . j1)] by A7, FUNCT_3:49 .= [s2,t2] by A3, A6 ; ::_thesis: verum end; theorem Th16: :: TOPALG_4:16 for S, T being non empty TopSpace for s1, s2 being Point of S for t1, t2 being Point of T st s1,s2 are_connected & t1,t2 are_connected holds for L1 being Path of s1,s2 for L2 being Path of t1,t2 holds <:L1,L2:> is Path of [s1,t1],[s2,t2] proof let S, T be non empty TopSpace; ::_thesis: for s1, s2 being Point of S for t1, t2 being Point of T st s1,s2 are_connected & t1,t2 are_connected holds for L1 being Path of s1,s2 for L2 being Path of t1,t2 holds <:L1,L2:> is Path of [s1,t1],[s2,t2] let s1, s2 be Point of S; ::_thesis: for t1, t2 being Point of T st s1,s2 are_connected & t1,t2 are_connected holds for L1 being Path of s1,s2 for L2 being Path of t1,t2 holds <:L1,L2:> is Path of [s1,t1],[s2,t2] let t1, t2 be Point of T; ::_thesis: ( s1,s2 are_connected & t1,t2 are_connected implies for L1 being Path of s1,s2 for L2 being Path of t1,t2 holds <:L1,L2:> is Path of [s1,t1],[s2,t2] ) assume that A1: s1,s2 are_connected and A2: t1,t2 are_connected ; ::_thesis: for L1 being Path of s1,s2 for L2 being Path of t1,t2 holds <:L1,L2:> is Path of [s1,t1],[s2,t2] let L1 be Path of s1,s2; ::_thesis: for L2 being Path of t1,t2 holds <:L1,L2:> is Path of [s1,t1],[s2,t2] let L2 be Path of t1,t2; ::_thesis: <:L1,L2:> is Path of [s1,t1],[s2,t2] ( L1 is continuous & L2 is continuous ) by A1, A2, BORSUK_2:def_2; then A3: <:L1,L2:> is continuous by YELLOW12:41; A4: ( dom L1 = the carrier of I[01] & dom L2 = the carrier of I[01] ) by FUNCT_2:def_1; then A5: <:L1,L2:> . j1 = [(L1 . j1),(L2 . j1)] by FUNCT_3:49 .= [s2,(L2 . j1)] by A1, BORSUK_2:def_2 .= [s2,t2] by A2, BORSUK_2:def_2 ; A6: <:L1,L2:> . j0 = [(L1 . j0),(L2 . j0)] by A4, FUNCT_3:49 .= [s1,(L2 . j0)] by A1, BORSUK_2:def_2 .= [s1,t1] by A2, BORSUK_2:def_2 ; then [s1,t1],[s2,t2] are_connected by A3, A5, BORSUK_2:def_1; hence <:L1,L2:> is Path of [s1,t1],[s2,t2] by A3, A6, A5, BORSUK_2:def_2; ::_thesis: verum end; definition let S, T be non empty pathwise_connected TopSpace; let s1, s2 be Point of S; let t1, t2 be Point of T; let L1 be Path of s1,s2; let L2 be Path of t1,t2; :: original: <: redefine func<:L1,L2:> -> Path of [s1,t1],[s2,t2]; coherence <:L1,L2:> is Path of [s1,t1],[s2,t2] proof ( s1,s2 are_connected & t1,t2 are_connected ) by BORSUK_2:def_3; hence <:L1,L2:> is Path of [s1,t1],[s2,t2] by Th16; ::_thesis: verum end; end; definition let S, T be non empty TopSpace; let s be Point of S; let t be Point of T; let L1 be Loop of s; let L2 be Loop of t; :: original: <: redefine func<:L1,L2:> -> Loop of [s,t]; coherence <:L1,L2:> is Loop of [s,t] by Th16; end; registration let S, T be non empty pathwise_connected TopSpace; cluster[:S,T:] -> pathwise_connected ; coherence [:S,T:] is pathwise_connected proof let a, b be Point of [:S,T:]; :: according to BORSUK_2:def_3 ::_thesis: a,b are_connected consider a1 being Point of S, a2 being Point of T such that A1: a = [a1,a2] by BORSUK_1:10; consider b1 being Point of S, b2 being Point of T such that A2: b = [b1,b2] by BORSUK_1:10; ( a1,b1 are_connected & a2,b2 are_connected ) by BORSUK_2:def_3; hence a,b are_connected by A1, A2, Th15; ::_thesis: verum end; end; definition let S, T be non empty pathwise_connected TopSpace; let s1, s2 be Point of S; let t1, t2 be Point of T; let L be Path of [s1,t1],[s2,t2]; :: original: pr1 redefine func pr1 L -> Path of s1,s2; coherence pr1 L is Path of s1,s2 proof [s1,t1],[s2,t2] are_connected by BORSUK_2:def_3; hence pr1 L is Path of s1,s2 by Th13; ::_thesis: verum end; :: original: pr2 redefine func pr2 L -> Path of t1,t2; coherence pr2 L is Path of t1,t2 proof [s1,t1],[s2,t2] are_connected by BORSUK_2:def_3; hence pr2 L is Path of t1,t2 by Th14; ::_thesis: verum end; end; definition let S, T be non empty TopSpace; let s be Point of S; let t be Point of T; let L be Loop of [s,t]; :: original: pr1 redefine func pr1 L -> Loop of s; coherence pr1 L is Loop of s by Th13; :: original: pr2 redefine func pr2 L -> Loop of t; coherence pr2 L is Loop of t by Th14; end; Lm3: for S, T being non empty TopSpace for s1, s2 being Point of S for t1, t2 being Point of T for l1, l2 being Path of [s1,t1],[s2,t2] for H being Homotopy of l1,l2 st l1,l2 are_homotopic holds ( pr1 H is continuous & ( for a being Point of I[01] holds ( (pr1 H) . (a,0) = (pr1 l1) . a & (pr1 H) . (a,1) = (pr1 l2) . a & ( for b being Point of I[01] holds ( (pr1 H) . (0,b) = s1 & (pr1 H) . (1,b) = s2 ) ) ) ) ) proof let S, T be non empty TopSpace; ::_thesis: for s1, s2 being Point of S for t1, t2 being Point of T for l1, l2 being Path of [s1,t1],[s2,t2] for H being Homotopy of l1,l2 st l1,l2 are_homotopic holds ( pr1 H is continuous & ( for a being Point of I[01] holds ( (pr1 H) . (a,0) = (pr1 l1) . a & (pr1 H) . (a,1) = (pr1 l2) . a & ( for b being Point of I[01] holds ( (pr1 H) . (0,b) = s1 & (pr1 H) . (1,b) = s2 ) ) ) ) ) let s1, s2 be Point of S; ::_thesis: for t1, t2 being Point of T for l1, l2 being Path of [s1,t1],[s2,t2] for H being Homotopy of l1,l2 st l1,l2 are_homotopic holds ( pr1 H is continuous & ( for a being Point of I[01] holds ( (pr1 H) . (a,0) = (pr1 l1) . a & (pr1 H) . (a,1) = (pr1 l2) . a & ( for b being Point of I[01] holds ( (pr1 H) . (0,b) = s1 & (pr1 H) . (1,b) = s2 ) ) ) ) ) let t1, t2 be Point of T; ::_thesis: for l1, l2 being Path of [s1,t1],[s2,t2] for H being Homotopy of l1,l2 st l1,l2 are_homotopic holds ( pr1 H is continuous & ( for a being Point of I[01] holds ( (pr1 H) . (a,0) = (pr1 l1) . a & (pr1 H) . (a,1) = (pr1 l2) . a & ( for b being Point of I[01] holds ( (pr1 H) . (0,b) = s1 & (pr1 H) . (1,b) = s2 ) ) ) ) ) let l1, l2 be Path of [s1,t1],[s2,t2]; ::_thesis: for H being Homotopy of l1,l2 st l1,l2 are_homotopic holds ( pr1 H is continuous & ( for a being Point of I[01] holds ( (pr1 H) . (a,0) = (pr1 l1) . a & (pr1 H) . (a,1) = (pr1 l2) . a & ( for b being Point of I[01] holds ( (pr1 H) . (0,b) = s1 & (pr1 H) . (1,b) = s2 ) ) ) ) ) let H be Homotopy of l1,l2; ::_thesis: ( l1,l2 are_homotopic implies ( pr1 H is continuous & ( for a being Point of I[01] holds ( (pr1 H) . (a,0) = (pr1 l1) . a & (pr1 H) . (a,1) = (pr1 l2) . a & ( for b being Point of I[01] holds ( (pr1 H) . (0,b) = s1 & (pr1 H) . (1,b) = s2 ) ) ) ) ) ) A1: dom l1 = the carrier of I[01] by FUNCT_2:def_1; A2: dom l2 = the carrier of I[01] by FUNCT_2:def_1; assume A3: l1,l2 are_homotopic ; ::_thesis: ( pr1 H is continuous & ( for a being Point of I[01] holds ( (pr1 H) . (a,0) = (pr1 l1) . a & (pr1 H) . (a,1) = (pr1 l2) . a & ( for b being Point of I[01] holds ( (pr1 H) . (0,b) = s1 & (pr1 H) . (1,b) = s2 ) ) ) ) ) then H is continuous by BORSUK_6:def_11; hence pr1 H is continuous by Th9; ::_thesis: for a being Point of I[01] holds ( (pr1 H) . (a,0) = (pr1 l1) . a & (pr1 H) . (a,1) = (pr1 l2) . a & ( for b being Point of I[01] holds ( (pr1 H) . (0,b) = s1 & (pr1 H) . (1,b) = s2 ) ) ) let a be Point of I[01]; ::_thesis: ( (pr1 H) . (a,0) = (pr1 l1) . a & (pr1 H) . (a,1) = (pr1 l2) . a & ( for b being Point of I[01] holds ( (pr1 H) . (0,b) = s1 & (pr1 H) . (1,b) = s2 ) ) ) A4: dom H = the carrier of [:I[01],I[01]:] by FUNCT_2:def_1; hence (pr1 H) . (a,0) = (H . [a,j0]) `1 by MCART_1:def_12 .= (H . (a,j0)) `1 .= (l1 . a) `1 by A3, BORSUK_6:def_11 .= (pr1 l1) . a by A1, MCART_1:def_12 ; ::_thesis: ( (pr1 H) . (a,1) = (pr1 l2) . a & ( for b being Point of I[01] holds ( (pr1 H) . (0,b) = s1 & (pr1 H) . (1,b) = s2 ) ) ) thus (pr1 H) . (a,1) = (H . [a,j1]) `1 by A4, MCART_1:def_12 .= (H . (a,j1)) `1 .= (l2 . a) `1 by A3, BORSUK_6:def_11 .= (pr1 l2) . a by A2, MCART_1:def_12 ; ::_thesis: for b being Point of I[01] holds ( (pr1 H) . (0,b) = s1 & (pr1 H) . (1,b) = s2 ) let b be Point of I[01]; ::_thesis: ( (pr1 H) . (0,b) = s1 & (pr1 H) . (1,b) = s2 ) thus (pr1 H) . (0,b) = (H . [j0,b]) `1 by A4, MCART_1:def_12 .= (H . (j0,b)) `1 .= [s1,t1] `1 by A3, BORSUK_6:def_11 .= s1 ; ::_thesis: (pr1 H) . (1,b) = s2 thus (pr1 H) . (1,b) = (H . [j1,b]) `1 by A4, MCART_1:def_12 .= (H . (j1,b)) `1 .= [s2,t2] `1 by A3, BORSUK_6:def_11 .= s2 ; ::_thesis: verum end; Lm4: for S, T being non empty TopSpace for s1, s2 being Point of S for t1, t2 being Point of T for l1, l2 being Path of [s1,t1],[s2,t2] for H being Homotopy of l1,l2 st l1,l2 are_homotopic holds ( pr2 H is continuous & ( for a being Point of I[01] holds ( (pr2 H) . (a,0) = (pr2 l1) . a & (pr2 H) . (a,1) = (pr2 l2) . a & ( for b being Point of I[01] holds ( (pr2 H) . (0,b) = t1 & (pr2 H) . (1,b) = t2 ) ) ) ) ) proof let S, T be non empty TopSpace; ::_thesis: for s1, s2 being Point of S for t1, t2 being Point of T for l1, l2 being Path of [s1,t1],[s2,t2] for H being Homotopy of l1,l2 st l1,l2 are_homotopic holds ( pr2 H is continuous & ( for a being Point of I[01] holds ( (pr2 H) . (a,0) = (pr2 l1) . a & (pr2 H) . (a,1) = (pr2 l2) . a & ( for b being Point of I[01] holds ( (pr2 H) . (0,b) = t1 & (pr2 H) . (1,b) = t2 ) ) ) ) ) let s1, s2 be Point of S; ::_thesis: for t1, t2 being Point of T for l1, l2 being Path of [s1,t1],[s2,t2] for H being Homotopy of l1,l2 st l1,l2 are_homotopic holds ( pr2 H is continuous & ( for a being Point of I[01] holds ( (pr2 H) . (a,0) = (pr2 l1) . a & (pr2 H) . (a,1) = (pr2 l2) . a & ( for b being Point of I[01] holds ( (pr2 H) . (0,b) = t1 & (pr2 H) . (1,b) = t2 ) ) ) ) ) let t1, t2 be Point of T; ::_thesis: for l1, l2 being Path of [s1,t1],[s2,t2] for H being Homotopy of l1,l2 st l1,l2 are_homotopic holds ( pr2 H is continuous & ( for a being Point of I[01] holds ( (pr2 H) . (a,0) = (pr2 l1) . a & (pr2 H) . (a,1) = (pr2 l2) . a & ( for b being Point of I[01] holds ( (pr2 H) . (0,b) = t1 & (pr2 H) . (1,b) = t2 ) ) ) ) ) let l1, l2 be Path of [s1,t1],[s2,t2]; ::_thesis: for H being Homotopy of l1,l2 st l1,l2 are_homotopic holds ( pr2 H is continuous & ( for a being Point of I[01] holds ( (pr2 H) . (a,0) = (pr2 l1) . a & (pr2 H) . (a,1) = (pr2 l2) . a & ( for b being Point of I[01] holds ( (pr2 H) . (0,b) = t1 & (pr2 H) . (1,b) = t2 ) ) ) ) ) let H be Homotopy of l1,l2; ::_thesis: ( l1,l2 are_homotopic implies ( pr2 H is continuous & ( for a being Point of I[01] holds ( (pr2 H) . (a,0) = (pr2 l1) . a & (pr2 H) . (a,1) = (pr2 l2) . a & ( for b being Point of I[01] holds ( (pr2 H) . (0,b) = t1 & (pr2 H) . (1,b) = t2 ) ) ) ) ) ) A1: dom l1 = the carrier of I[01] by FUNCT_2:def_1; A2: dom l2 = the carrier of I[01] by FUNCT_2:def_1; assume A3: l1,l2 are_homotopic ; ::_thesis: ( pr2 H is continuous & ( for a being Point of I[01] holds ( (pr2 H) . (a,0) = (pr2 l1) . a & (pr2 H) . (a,1) = (pr2 l2) . a & ( for b being Point of I[01] holds ( (pr2 H) . (0,b) = t1 & (pr2 H) . (1,b) = t2 ) ) ) ) ) then H is continuous by BORSUK_6:def_11; hence pr2 H is continuous by Th10; ::_thesis: for a being Point of I[01] holds ( (pr2 H) . (a,0) = (pr2 l1) . a & (pr2 H) . (a,1) = (pr2 l2) . a & ( for b being Point of I[01] holds ( (pr2 H) . (0,b) = t1 & (pr2 H) . (1,b) = t2 ) ) ) let a be Point of I[01]; ::_thesis: ( (pr2 H) . (a,0) = (pr2 l1) . a & (pr2 H) . (a,1) = (pr2 l2) . a & ( for b being Point of I[01] holds ( (pr2 H) . (0,b) = t1 & (pr2 H) . (1,b) = t2 ) ) ) A4: dom H = the carrier of [:I[01],I[01]:] by FUNCT_2:def_1; hence (pr2 H) . (a,0) = (H . [a,j0]) `2 by MCART_1:def_13 .= (H . (a,j0)) `2 .= (l1 . a) `2 by A3, BORSUK_6:def_11 .= (pr2 l1) . a by A1, MCART_1:def_13 ; ::_thesis: ( (pr2 H) . (a,1) = (pr2 l2) . a & ( for b being Point of I[01] holds ( (pr2 H) . (0,b) = t1 & (pr2 H) . (1,b) = t2 ) ) ) thus (pr2 H) . (a,1) = (H . [a,j1]) `2 by A4, MCART_1:def_13 .= (H . (a,j1)) `2 .= (l2 . a) `2 by A3, BORSUK_6:def_11 .= (pr2 l2) . a by A2, MCART_1:def_13 ; ::_thesis: for b being Point of I[01] holds ( (pr2 H) . (0,b) = t1 & (pr2 H) . (1,b) = t2 ) let b be Point of I[01]; ::_thesis: ( (pr2 H) . (0,b) = t1 & (pr2 H) . (1,b) = t2 ) thus (pr2 H) . (0,b) = (H . [j0,b]) `2 by A4, MCART_1:def_13 .= (H . (j0,b)) `2 .= [s1,t1] `2 by A3, BORSUK_6:def_11 .= t1 ; ::_thesis: (pr2 H) . (1,b) = t2 thus (pr2 H) . (1,b) = (H . [j1,b]) `2 by A4, MCART_1:def_13 .= (H . (j1,b)) `2 .= [s2,t2] `2 by A3, BORSUK_6:def_11 .= t2 ; ::_thesis: verum end; theorem :: TOPALG_4:17 for S, T being non empty TopSpace for s1, s2 being Point of S for t1, t2 being Point of T for l1, l2 being Path of [s1,t1],[s2,t2] for H being Homotopy of l1,l2 for p, q being Path of s1,s2 st p = pr1 l1 & q = pr1 l2 & l1,l2 are_homotopic holds pr1 H is Homotopy of p,q proof let S, T be non empty TopSpace; ::_thesis: for s1, s2 being Point of S for t1, t2 being Point of T for l1, l2 being Path of [s1,t1],[s2,t2] for H being Homotopy of l1,l2 for p, q being Path of s1,s2 st p = pr1 l1 & q = pr1 l2 & l1,l2 are_homotopic holds pr1 H is Homotopy of p,q let s1, s2 be Point of S; ::_thesis: for t1, t2 being Point of T for l1, l2 being Path of [s1,t1],[s2,t2] for H being Homotopy of l1,l2 for p, q being Path of s1,s2 st p = pr1 l1 & q = pr1 l2 & l1,l2 are_homotopic holds pr1 H is Homotopy of p,q let t1, t2 be Point of T; ::_thesis: for l1, l2 being Path of [s1,t1],[s2,t2] for H being Homotopy of l1,l2 for p, q being Path of s1,s2 st p = pr1 l1 & q = pr1 l2 & l1,l2 are_homotopic holds pr1 H is Homotopy of p,q let l1, l2 be Path of [s1,t1],[s2,t2]; ::_thesis: for H being Homotopy of l1,l2 for p, q being Path of s1,s2 st p = pr1 l1 & q = pr1 l2 & l1,l2 are_homotopic holds pr1 H is Homotopy of p,q let H be Homotopy of l1,l2; ::_thesis: for p, q being Path of s1,s2 st p = pr1 l1 & q = pr1 l2 & l1,l2 are_homotopic holds pr1 H is Homotopy of p,q let p, q be Path of s1,s2; ::_thesis: ( p = pr1 l1 & q = pr1 l2 & l1,l2 are_homotopic implies pr1 H is Homotopy of p,q ) assume A1: ( p = pr1 l1 & q = pr1 l2 & l1,l2 are_homotopic ) ; ::_thesis: pr1 H is Homotopy of p,q thus p,q are_homotopic :: according to BORSUK_6:def_11 ::_thesis: ( pr1 H is continuous & ( for b1 being M2( the carrier of K554()) holds ( (pr1 H) . (b1,0) = p . b1 & (pr1 H) . (b1,1) = q . b1 & (pr1 H) . (0,b1) = s1 & (pr1 H) . (1,b1) = s2 ) ) ) proof take pr1 H ; :: according to BORSUK_2:def_7 ::_thesis: ( pr1 H is continuous & ( for b1 being M2( the carrier of K554()) holds ( (pr1 H) . (b1,0) = p . b1 & (pr1 H) . (b1,1) = q . b1 & (pr1 H) . (0,b1) = s1 & (pr1 H) . (1,b1) = s2 ) ) ) thus ( pr1 H is continuous & ( for b1 being M2( the carrier of K554()) holds ( (pr1 H) . (b1,0) = p . b1 & (pr1 H) . (b1,1) = q . b1 & (pr1 H) . (0,b1) = s1 & (pr1 H) . (1,b1) = s2 ) ) ) by A1, Lm3; ::_thesis: verum end; thus ( pr1 H is continuous & ( for b1 being M2( the carrier of K554()) holds ( (pr1 H) . (b1,0) = p . b1 & (pr1 H) . (b1,1) = q . b1 & (pr1 H) . (0,b1) = s1 & (pr1 H) . (1,b1) = s2 ) ) ) by A1, Lm3; ::_thesis: verum end; theorem :: TOPALG_4:18 for S, T being non empty TopSpace for s1, s2 being Point of S for t1, t2 being Point of T for l1, l2 being Path of [s1,t1],[s2,t2] for H being Homotopy of l1,l2 for p, q being Path of t1,t2 st p = pr2 l1 & q = pr2 l2 & l1,l2 are_homotopic holds pr2 H is Homotopy of p,q proof let S, T be non empty TopSpace; ::_thesis: for s1, s2 being Point of S for t1, t2 being Point of T for l1, l2 being Path of [s1,t1],[s2,t2] for H being Homotopy of l1,l2 for p, q being Path of t1,t2 st p = pr2 l1 & q = pr2 l2 & l1,l2 are_homotopic holds pr2 H is Homotopy of p,q let s1, s2 be Point of S; ::_thesis: for t1, t2 being Point of T for l1, l2 being Path of [s1,t1],[s2,t2] for H being Homotopy of l1,l2 for p, q being Path of t1,t2 st p = pr2 l1 & q = pr2 l2 & l1,l2 are_homotopic holds pr2 H is Homotopy of p,q let t1, t2 be Point of T; ::_thesis: for l1, l2 being Path of [s1,t1],[s2,t2] for H being Homotopy of l1,l2 for p, q being Path of t1,t2 st p = pr2 l1 & q = pr2 l2 & l1,l2 are_homotopic holds pr2 H is Homotopy of p,q let l1, l2 be Path of [s1,t1],[s2,t2]; ::_thesis: for H being Homotopy of l1,l2 for p, q being Path of t1,t2 st p = pr2 l1 & q = pr2 l2 & l1,l2 are_homotopic holds pr2 H is Homotopy of p,q let H be Homotopy of l1,l2; ::_thesis: for p, q being Path of t1,t2 st p = pr2 l1 & q = pr2 l2 & l1,l2 are_homotopic holds pr2 H is Homotopy of p,q let p, q be Path of t1,t2; ::_thesis: ( p = pr2 l1 & q = pr2 l2 & l1,l2 are_homotopic implies pr2 H is Homotopy of p,q ) assume A1: ( p = pr2 l1 & q = pr2 l2 & l1,l2 are_homotopic ) ; ::_thesis: pr2 H is Homotopy of p,q thus p,q are_homotopic :: according to BORSUK_6:def_11 ::_thesis: ( pr2 H is continuous & ( for b1 being M2( the carrier of K554()) holds ( (pr2 H) . (b1,0) = p . b1 & (pr2 H) . (b1,1) = q . b1 & (pr2 H) . (0,b1) = t1 & (pr2 H) . (1,b1) = t2 ) ) ) proof take pr2 H ; :: according to BORSUK_2:def_7 ::_thesis: ( pr2 H is continuous & ( for b1 being M2( the carrier of K554()) holds ( (pr2 H) . (b1,0) = p . b1 & (pr2 H) . (b1,1) = q . b1 & (pr2 H) . (0,b1) = t1 & (pr2 H) . (1,b1) = t2 ) ) ) thus ( pr2 H is continuous & ( for b1 being M2( the carrier of K554()) holds ( (pr2 H) . (b1,0) = p . b1 & (pr2 H) . (b1,1) = q . b1 & (pr2 H) . (0,b1) = t1 & (pr2 H) . (1,b1) = t2 ) ) ) by A1, Lm4; ::_thesis: verum end; thus ( pr2 H is continuous & ( for b1 being M2( the carrier of K554()) holds ( (pr2 H) . (b1,0) = p . b1 & (pr2 H) . (b1,1) = q . b1 & (pr2 H) . (0,b1) = t1 & (pr2 H) . (1,b1) = t2 ) ) ) by A1, Lm4; ::_thesis: verum end; theorem Th19: :: TOPALG_4:19 for S, T being non empty TopSpace for s1, s2 being Point of S for t1, t2 being Point of T for l1, l2 being Path of [s1,t1],[s2,t2] for p, q being Path of s1,s2 st p = pr1 l1 & q = pr1 l2 & l1,l2 are_homotopic holds p,q are_homotopic proof let S, T be non empty TopSpace; ::_thesis: for s1, s2 being Point of S for t1, t2 being Point of T for l1, l2 being Path of [s1,t1],[s2,t2] for p, q being Path of s1,s2 st p = pr1 l1 & q = pr1 l2 & l1,l2 are_homotopic holds p,q are_homotopic let s1, s2 be Point of S; ::_thesis: for t1, t2 being Point of T for l1, l2 being Path of [s1,t1],[s2,t2] for p, q being Path of s1,s2 st p = pr1 l1 & q = pr1 l2 & l1,l2 are_homotopic holds p,q are_homotopic let t1, t2 be Point of T; ::_thesis: for l1, l2 being Path of [s1,t1],[s2,t2] for p, q being Path of s1,s2 st p = pr1 l1 & q = pr1 l2 & l1,l2 are_homotopic holds p,q are_homotopic let l1, l2 be Path of [s1,t1],[s2,t2]; ::_thesis: for p, q being Path of s1,s2 st p = pr1 l1 & q = pr1 l2 & l1,l2 are_homotopic holds p,q are_homotopic let p, q be Path of s1,s2; ::_thesis: ( p = pr1 l1 & q = pr1 l2 & l1,l2 are_homotopic implies p,q are_homotopic ) assume that A1: ( p = pr1 l1 & q = pr1 l2 ) and A2: l1,l2 are_homotopic ; ::_thesis: p,q are_homotopic consider f being Function of [:I[01],I[01]:],[:S,T:] such that A3: ( f is continuous & ( for a being Point of I[01] holds ( f . (a,0) = l1 . a & f . (a,1) = l2 . a & ( for b being Point of I[01] holds ( f . (0,b) = [s1,t1] & f . (1,b) = [s2,t2] ) ) ) ) ) by A2, BORSUK_2:def_7; take pr1 f ; :: according to BORSUK_2:def_7 ::_thesis: ( pr1 f is continuous & ( for b1 being M2( the carrier of K554()) holds ( (pr1 f) . (b1,0) = p . b1 & (pr1 f) . (b1,1) = q . b1 & (pr1 f) . (0,b1) = s1 & (pr1 f) . (1,b1) = s2 ) ) ) f is Homotopy of l1,l2 by A2, A3, BORSUK_6:def_11; hence ( pr1 f is continuous & ( for b1 being M2( the carrier of K554()) holds ( (pr1 f) . (b1,0) = p . b1 & (pr1 f) . (b1,1) = q . b1 & (pr1 f) . (0,b1) = s1 & (pr1 f) . (1,b1) = s2 ) ) ) by A1, A2, Lm3; ::_thesis: verum end; theorem Th20: :: TOPALG_4:20 for S, T being non empty TopSpace for s1, s2 being Point of S for t1, t2 being Point of T for l1, l2 being Path of [s1,t1],[s2,t2] for p, q being Path of t1,t2 st p = pr2 l1 & q = pr2 l2 & l1,l2 are_homotopic holds p,q are_homotopic proof let S, T be non empty TopSpace; ::_thesis: for s1, s2 being Point of S for t1, t2 being Point of T for l1, l2 being Path of [s1,t1],[s2,t2] for p, q being Path of t1,t2 st p = pr2 l1 & q = pr2 l2 & l1,l2 are_homotopic holds p,q are_homotopic let s1, s2 be Point of S; ::_thesis: for t1, t2 being Point of T for l1, l2 being Path of [s1,t1],[s2,t2] for p, q being Path of t1,t2 st p = pr2 l1 & q = pr2 l2 & l1,l2 are_homotopic holds p,q are_homotopic let t1, t2 be Point of T; ::_thesis: for l1, l2 being Path of [s1,t1],[s2,t2] for p, q being Path of t1,t2 st p = pr2 l1 & q = pr2 l2 & l1,l2 are_homotopic holds p,q are_homotopic let l1, l2 be Path of [s1,t1],[s2,t2]; ::_thesis: for p, q being Path of t1,t2 st p = pr2 l1 & q = pr2 l2 & l1,l2 are_homotopic holds p,q are_homotopic let p, q be Path of t1,t2; ::_thesis: ( p = pr2 l1 & q = pr2 l2 & l1,l2 are_homotopic implies p,q are_homotopic ) assume that A1: ( p = pr2 l1 & q = pr2 l2 ) and A2: l1,l2 are_homotopic ; ::_thesis: p,q are_homotopic consider f being Function of [:I[01],I[01]:],[:S,T:] such that A3: ( f is continuous & ( for a being Point of I[01] holds ( f . (a,0) = l1 . a & f . (a,1) = l2 . a & ( for b being Point of I[01] holds ( f . (0,b) = [s1,t1] & f . (1,b) = [s2,t2] ) ) ) ) ) by A2, BORSUK_2:def_7; take pr2 f ; :: according to BORSUK_2:def_7 ::_thesis: ( pr2 f is continuous & ( for b1 being M2( the carrier of K554()) holds ( (pr2 f) . (b1,0) = p . b1 & (pr2 f) . (b1,1) = q . b1 & (pr2 f) . (0,b1) = t1 & (pr2 f) . (1,b1) = t2 ) ) ) f is Homotopy of l1,l2 by A2, A3, BORSUK_6:def_11; hence ( pr2 f is continuous & ( for b1 being M2( the carrier of K554()) holds ( (pr2 f) . (b1,0) = p . b1 & (pr2 f) . (b1,1) = q . b1 & (pr2 f) . (0,b1) = t1 & (pr2 f) . (1,b1) = t2 ) ) ) by A1, A2, Lm4; ::_thesis: verum end; Lm5: for S, T being non empty TopSpace for s1, s2 being Point of S for t1, t2 being Point of T for l1, l2 being Path of [s1,t1],[s2,t2] for p, q being Path of s1,s2 for x, y being Path of t1,t2 for f being Homotopy of p,q for g being Homotopy of x,y st p = pr1 l1 & q = pr1 l2 & x = pr2 l1 & y = pr2 l2 & p,q are_homotopic & x,y are_homotopic holds ( <:f,g:> is continuous & ( for a being Point of I[01] holds ( <:f,g:> . (a,0) = l1 . a & <:f,g:> . (a,1) = l2 . a & ( for b being Point of I[01] holds ( <:f,g:> . (0,b) = [s1,t1] & <:f,g:> . (1,b) = [s2,t2] ) ) ) ) ) proof let S, T be non empty TopSpace; ::_thesis: for s1, s2 being Point of S for t1, t2 being Point of T for l1, l2 being Path of [s1,t1],[s2,t2] for p, q being Path of s1,s2 for x, y being Path of t1,t2 for f being Homotopy of p,q for g being Homotopy of x,y st p = pr1 l1 & q = pr1 l2 & x = pr2 l1 & y = pr2 l2 & p,q are_homotopic & x,y are_homotopic holds ( <:f,g:> is continuous & ( for a being Point of I[01] holds ( <:f,g:> . (a,0) = l1 . a & <:f,g:> . (a,1) = l2 . a & ( for b being Point of I[01] holds ( <:f,g:> . (0,b) = [s1,t1] & <:f,g:> . (1,b) = [s2,t2] ) ) ) ) ) let s1, s2 be Point of S; ::_thesis: for t1, t2 being Point of T for l1, l2 being Path of [s1,t1],[s2,t2] for p, q being Path of s1,s2 for x, y being Path of t1,t2 for f being Homotopy of p,q for g being Homotopy of x,y st p = pr1 l1 & q = pr1 l2 & x = pr2 l1 & y = pr2 l2 & p,q are_homotopic & x,y are_homotopic holds ( <:f,g:> is continuous & ( for a being Point of I[01] holds ( <:f,g:> . (a,0) = l1 . a & <:f,g:> . (a,1) = l2 . a & ( for b being Point of I[01] holds ( <:f,g:> . (0,b) = [s1,t1] & <:f,g:> . (1,b) = [s2,t2] ) ) ) ) ) let t1, t2 be Point of T; ::_thesis: for l1, l2 being Path of [s1,t1],[s2,t2] for p, q being Path of s1,s2 for x, y being Path of t1,t2 for f being Homotopy of p,q for g being Homotopy of x,y st p = pr1 l1 & q = pr1 l2 & x = pr2 l1 & y = pr2 l2 & p,q are_homotopic & x,y are_homotopic holds ( <:f,g:> is continuous & ( for a being Point of I[01] holds ( <:f,g:> . (a,0) = l1 . a & <:f,g:> . (a,1) = l2 . a & ( for b being Point of I[01] holds ( <:f,g:> . (0,b) = [s1,t1] & <:f,g:> . (1,b) = [s2,t2] ) ) ) ) ) let l1, l2 be Path of [s1,t1],[s2,t2]; ::_thesis: for p, q being Path of s1,s2 for x, y being Path of t1,t2 for f being Homotopy of p,q for g being Homotopy of x,y st p = pr1 l1 & q = pr1 l2 & x = pr2 l1 & y = pr2 l2 & p,q are_homotopic & x,y are_homotopic holds ( <:f,g:> is continuous & ( for a being Point of I[01] holds ( <:f,g:> . (a,0) = l1 . a & <:f,g:> . (a,1) = l2 . a & ( for b being Point of I[01] holds ( <:f,g:> . (0,b) = [s1,t1] & <:f,g:> . (1,b) = [s2,t2] ) ) ) ) ) let p, q be Path of s1,s2; ::_thesis: for x, y being Path of t1,t2 for f being Homotopy of p,q for g being Homotopy of x,y st p = pr1 l1 & q = pr1 l2 & x = pr2 l1 & y = pr2 l2 & p,q are_homotopic & x,y are_homotopic holds ( <:f,g:> is continuous & ( for a being Point of I[01] holds ( <:f,g:> . (a,0) = l1 . a & <:f,g:> . (a,1) = l2 . a & ( for b being Point of I[01] holds ( <:f,g:> . (0,b) = [s1,t1] & <:f,g:> . (1,b) = [s2,t2] ) ) ) ) ) let x, y be Path of t1,t2; ::_thesis: for f being Homotopy of p,q for g being Homotopy of x,y st p = pr1 l1 & q = pr1 l2 & x = pr2 l1 & y = pr2 l2 & p,q are_homotopic & x,y are_homotopic holds ( <:f,g:> is continuous & ( for a being Point of I[01] holds ( <:f,g:> . (a,0) = l1 . a & <:f,g:> . (a,1) = l2 . a & ( for b being Point of I[01] holds ( <:f,g:> . (0,b) = [s1,t1] & <:f,g:> . (1,b) = [s2,t2] ) ) ) ) ) let f be Homotopy of p,q; ::_thesis: for g being Homotopy of x,y st p = pr1 l1 & q = pr1 l2 & x = pr2 l1 & y = pr2 l2 & p,q are_homotopic & x,y are_homotopic holds ( <:f,g:> is continuous & ( for a being Point of I[01] holds ( <:f,g:> . (a,0) = l1 . a & <:f,g:> . (a,1) = l2 . a & ( for b being Point of I[01] holds ( <:f,g:> . (0,b) = [s1,t1] & <:f,g:> . (1,b) = [s2,t2] ) ) ) ) ) let g be Homotopy of x,y; ::_thesis: ( p = pr1 l1 & q = pr1 l2 & x = pr2 l1 & y = pr2 l2 & p,q are_homotopic & x,y are_homotopic implies ( <:f,g:> is continuous & ( for a being Point of I[01] holds ( <:f,g:> . (a,0) = l1 . a & <:f,g:> . (a,1) = l2 . a & ( for b being Point of I[01] holds ( <:f,g:> . (0,b) = [s1,t1] & <:f,g:> . (1,b) = [s2,t2] ) ) ) ) ) ) assume that A1: p = pr1 l1 and A2: q = pr1 l2 and A3: x = pr2 l1 and A4: y = pr2 l2 and A5: p,q are_homotopic and A6: x,y are_homotopic ; ::_thesis: ( <:f,g:> is continuous & ( for a being Point of I[01] holds ( <:f,g:> . (a,0) = l1 . a & <:f,g:> . (a,1) = l2 . a & ( for b being Point of I[01] holds ( <:f,g:> . (0,b) = [s1,t1] & <:f,g:> . (1,b) = [s2,t2] ) ) ) ) ) set h = <:f,g:>; ( f is continuous & g is continuous ) by A5, A6, BORSUK_6:def_11; hence <:f,g:> is continuous by YELLOW12:41; ::_thesis: for a being Point of I[01] holds ( <:f,g:> . (a,0) = l1 . a & <:f,g:> . (a,1) = l2 . a & ( for b being Point of I[01] holds ( <:f,g:> . (0,b) = [s1,t1] & <:f,g:> . (1,b) = [s2,t2] ) ) ) let a be Point of I[01]; ::_thesis: ( <:f,g:> . (a,0) = l1 . a & <:f,g:> . (a,1) = l2 . a & ( for b being Point of I[01] holds ( <:f,g:> . (0,b) = [s1,t1] & <:f,g:> . (1,b) = [s2,t2] ) ) ) A7: dom l1 = the carrier of I[01] by FUNCT_2:def_1; A8: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by BORSUK_1:def_2; A9: ( dom f = the carrier of [:I[01],I[01]:] & dom g = the carrier of [:I[01],I[01]:] ) by FUNCT_2:def_1; hence <:f,g:> . (a,0) = [(f . [a,j0]),(g . [a,j0])] by FUNCT_3:49 .= [(f . (a,j0)),(g . (a,j0))] .= [((pr1 l1) . a),(g . (a,j0))] by A1, A5, BORSUK_6:def_11 .= [((pr1 l1) . a),((pr2 l1) . a)] by A3, A6, BORSUK_6:def_11 .= [((l1 . a) `1),((pr2 l1) . a)] by A7, MCART_1:def_12 .= [((l1 . a) `1),((l1 . a) `2)] by A7, MCART_1:def_13 .= l1 . a by A8, MCART_1:21 ; ::_thesis: ( <:f,g:> . (a,1) = l2 . a & ( for b being Point of I[01] holds ( <:f,g:> . (0,b) = [s1,t1] & <:f,g:> . (1,b) = [s2,t2] ) ) ) A10: dom l2 = the carrier of I[01] by FUNCT_2:def_1; thus <:f,g:> . (a,1) = [(f . [a,j1]),(g . [a,j1])] by A9, FUNCT_3:49 .= [(f . (a,j1)),(g . (a,j1))] .= [((pr1 l2) . a),(g . (a,j1))] by A2, A5, BORSUK_6:def_11 .= [((pr1 l2) . a),((pr2 l2) . a)] by A4, A6, BORSUK_6:def_11 .= [((l2 . a) `1),((pr2 l2) . a)] by A10, MCART_1:def_12 .= [((l2 . a) `1),((l2 . a) `2)] by A10, MCART_1:def_13 .= l2 . a by A8, MCART_1:21 ; ::_thesis: for b being Point of I[01] holds ( <:f,g:> . (0,b) = [s1,t1] & <:f,g:> . (1,b) = [s2,t2] ) let b be Point of I[01]; ::_thesis: ( <:f,g:> . (0,b) = [s1,t1] & <:f,g:> . (1,b) = [s2,t2] ) thus <:f,g:> . (0,b) = [(f . [j0,b]),(g . [j0,b])] by A9, FUNCT_3:49 .= [(f . (j0,b)),(g . (j0,b))] .= [s1,(g . (j0,b))] by A5, BORSUK_6:def_11 .= [s1,t1] by A6, BORSUK_6:def_11 ; ::_thesis: <:f,g:> . (1,b) = [s2,t2] thus <:f,g:> . (1,b) = [(f . [j1,b]),(g . [j1,b])] by A9, FUNCT_3:49 .= [(f . (j1,b)),(g . (j1,b))] .= [s2,(g . (j1,b))] by A5, BORSUK_6:def_11 .= [s2,t2] by A6, BORSUK_6:def_11 ; ::_thesis: verum end; theorem :: TOPALG_4:21 for S, T being non empty TopSpace for s1, s2 being Point of S for t1, t2 being Point of T for l1, l2 being Path of [s1,t1],[s2,t2] for p, q being Path of s1,s2 for x, y being Path of t1,t2 for f being Homotopy of p,q for g being Homotopy of x,y st p = pr1 l1 & q = pr1 l2 & x = pr2 l1 & y = pr2 l2 & p,q are_homotopic & x,y are_homotopic holds <:f,g:> is Homotopy of l1,l2 proof let S, T be non empty TopSpace; ::_thesis: for s1, s2 being Point of S for t1, t2 being Point of T for l1, l2 being Path of [s1,t1],[s2,t2] for p, q being Path of s1,s2 for x, y being Path of t1,t2 for f being Homotopy of p,q for g being Homotopy of x,y st p = pr1 l1 & q = pr1 l2 & x = pr2 l1 & y = pr2 l2 & p,q are_homotopic & x,y are_homotopic holds <:f,g:> is Homotopy of l1,l2 let s1, s2 be Point of S; ::_thesis: for t1, t2 being Point of T for l1, l2 being Path of [s1,t1],[s2,t2] for p, q being Path of s1,s2 for x, y being Path of t1,t2 for f being Homotopy of p,q for g being Homotopy of x,y st p = pr1 l1 & q = pr1 l2 & x = pr2 l1 & y = pr2 l2 & p,q are_homotopic & x,y are_homotopic holds <:f,g:> is Homotopy of l1,l2 let t1, t2 be Point of T; ::_thesis: for l1, l2 being Path of [s1,t1],[s2,t2] for p, q being Path of s1,s2 for x, y being Path of t1,t2 for f being Homotopy of p,q for g being Homotopy of x,y st p = pr1 l1 & q = pr1 l2 & x = pr2 l1 & y = pr2 l2 & p,q are_homotopic & x,y are_homotopic holds <:f,g:> is Homotopy of l1,l2 let l1, l2 be Path of [s1,t1],[s2,t2]; ::_thesis: for p, q being Path of s1,s2 for x, y being Path of t1,t2 for f being Homotopy of p,q for g being Homotopy of x,y st p = pr1 l1 & q = pr1 l2 & x = pr2 l1 & y = pr2 l2 & p,q are_homotopic & x,y are_homotopic holds <:f,g:> is Homotopy of l1,l2 let p, q be Path of s1,s2; ::_thesis: for x, y being Path of t1,t2 for f being Homotopy of p,q for g being Homotopy of x,y st p = pr1 l1 & q = pr1 l2 & x = pr2 l1 & y = pr2 l2 & p,q are_homotopic & x,y are_homotopic holds <:f,g:> is Homotopy of l1,l2 let x, y be Path of t1,t2; ::_thesis: for f being Homotopy of p,q for g being Homotopy of x,y st p = pr1 l1 & q = pr1 l2 & x = pr2 l1 & y = pr2 l2 & p,q are_homotopic & x,y are_homotopic holds <:f,g:> is Homotopy of l1,l2 let f be Homotopy of p,q; ::_thesis: for g being Homotopy of x,y st p = pr1 l1 & q = pr1 l2 & x = pr2 l1 & y = pr2 l2 & p,q are_homotopic & x,y are_homotopic holds <:f,g:> is Homotopy of l1,l2 let g be Homotopy of x,y; ::_thesis: ( p = pr1 l1 & q = pr1 l2 & x = pr2 l1 & y = pr2 l2 & p,q are_homotopic & x,y are_homotopic implies <:f,g:> is Homotopy of l1,l2 ) assume A1: ( p = pr1 l1 & q = pr1 l2 & x = pr2 l1 & y = pr2 l2 & p,q are_homotopic & x,y are_homotopic ) ; ::_thesis: <:f,g:> is Homotopy of l1,l2 thus l1,l2 are_homotopic :: according to BORSUK_6:def_11 ::_thesis: ( <:f,g:> is continuous & ( for b1 being M2( the carrier of K554()) holds ( <:f,g:> . (b1,0) = l1 . b1 & <:f,g:> . (b1,1) = l2 . b1 & <:f,g:> . (0,b1) = [s1,t1] & <:f,g:> . (1,b1) = [s2,t2] ) ) ) proof take <:f,g:> ; :: according to BORSUK_2:def_7 ::_thesis: ( <:f,g:> is continuous & ( for b1 being M2( the carrier of K554()) holds ( <:f,g:> . (b1,0) = l1 . b1 & <:f,g:> . (b1,1) = l2 . b1 & <:f,g:> . (0,b1) = [s1,t1] & <:f,g:> . (1,b1) = [s2,t2] ) ) ) thus ( <:f,g:> is continuous & ( for b1 being M2( the carrier of K554()) holds ( <:f,g:> . (b1,0) = l1 . b1 & <:f,g:> . (b1,1) = l2 . b1 & <:f,g:> . (0,b1) = [s1,t1] & <:f,g:> . (1,b1) = [s2,t2] ) ) ) by A1, Lm5; ::_thesis: verum end; thus ( <:f,g:> is continuous & ( for b1 being M2( the carrier of K554()) holds ( <:f,g:> . (b1,0) = l1 . b1 & <:f,g:> . (b1,1) = l2 . b1 & <:f,g:> . (0,b1) = [s1,t1] & <:f,g:> . (1,b1) = [s2,t2] ) ) ) by A1, Lm5; ::_thesis: verum end; theorem Th22: :: TOPALG_4:22 for S, T being non empty TopSpace for s1, s2 being Point of S for t1, t2 being Point of T for l1, l2 being Path of [s1,t1],[s2,t2] for p, q being Path of s1,s2 for x, y being Path of t1,t2 st p = pr1 l1 & q = pr1 l2 & x = pr2 l1 & y = pr2 l2 & p,q are_homotopic & x,y are_homotopic holds l1,l2 are_homotopic proof let S, T be non empty TopSpace; ::_thesis: for s1, s2 being Point of S for t1, t2 being Point of T for l1, l2 being Path of [s1,t1],[s2,t2] for p, q being Path of s1,s2 for x, y being Path of t1,t2 st p = pr1 l1 & q = pr1 l2 & x = pr2 l1 & y = pr2 l2 & p,q are_homotopic & x,y are_homotopic holds l1,l2 are_homotopic let s1, s2 be Point of S; ::_thesis: for t1, t2 being Point of T for l1, l2 being Path of [s1,t1],[s2,t2] for p, q being Path of s1,s2 for x, y being Path of t1,t2 st p = pr1 l1 & q = pr1 l2 & x = pr2 l1 & y = pr2 l2 & p,q are_homotopic & x,y are_homotopic holds l1,l2 are_homotopic let t1, t2 be Point of T; ::_thesis: for l1, l2 being Path of [s1,t1],[s2,t2] for p, q being Path of s1,s2 for x, y being Path of t1,t2 st p = pr1 l1 & q = pr1 l2 & x = pr2 l1 & y = pr2 l2 & p,q are_homotopic & x,y are_homotopic holds l1,l2 are_homotopic let l1, l2 be Path of [s1,t1],[s2,t2]; ::_thesis: for p, q being Path of s1,s2 for x, y being Path of t1,t2 st p = pr1 l1 & q = pr1 l2 & x = pr2 l1 & y = pr2 l2 & p,q are_homotopic & x,y are_homotopic holds l1,l2 are_homotopic let p, q be Path of s1,s2; ::_thesis: for x, y being Path of t1,t2 st p = pr1 l1 & q = pr1 l2 & x = pr2 l1 & y = pr2 l2 & p,q are_homotopic & x,y are_homotopic holds l1,l2 are_homotopic let x, y be Path of t1,t2; ::_thesis: ( p = pr1 l1 & q = pr1 l2 & x = pr2 l1 & y = pr2 l2 & p,q are_homotopic & x,y are_homotopic implies l1,l2 are_homotopic ) assume that A1: ( p = pr1 l1 & q = pr1 l2 ) and A2: ( x = pr2 l1 & y = pr2 l2 ) and A3: p,q are_homotopic and A4: x,y are_homotopic ; ::_thesis: l1,l2 are_homotopic consider g being Function of [:I[01],I[01]:],T such that A5: ( g is continuous & ( for a being Point of I[01] holds ( g . (a,0) = (pr2 l1) . a & g . (a,1) = (pr2 l2) . a & ( for b being Point of I[01] holds ( g . (0,b) = t1 & g . (1,b) = t2 ) ) ) ) ) by A2, A4, BORSUK_2:def_7; A6: g is Homotopy of x,y by A2, A4, A5, BORSUK_6:def_11; consider f being Function of [:I[01],I[01]:],S such that A7: ( f is continuous & ( for a being Point of I[01] holds ( f . (a,0) = (pr1 l1) . a & f . (a,1) = (pr1 l2) . a & ( for b being Point of I[01] holds ( f . (0,b) = s1 & f . (1,b) = s2 ) ) ) ) ) by A1, A3, BORSUK_2:def_7; take <:f,g:> ; :: according to BORSUK_2:def_7 ::_thesis: ( <:f,g:> is continuous & ( for b1 being M2( the carrier of K554()) holds ( <:f,g:> . (b1,0) = l1 . b1 & <:f,g:> . (b1,1) = l2 . b1 & <:f,g:> . (0,b1) = [s1,t1] & <:f,g:> . (1,b1) = [s2,t2] ) ) ) f is Homotopy of p,q by A1, A3, A7, BORSUK_6:def_11; hence ( <:f,g:> is continuous & ( for b1 being M2( the carrier of K554()) holds ( <:f,g:> . (b1,0) = l1 . b1 & <:f,g:> . (b1,1) = l2 . b1 & <:f,g:> . (0,b1) = [s1,t1] & <:f,g:> . (1,b1) = [s2,t2] ) ) ) by A1, A2, A3, A4, A6, Lm5; ::_thesis: verum end; theorem Th23: :: TOPALG_4:23 for S, T being non empty TopSpace for s1, s2, s3 being Point of S for t1, t2, t3 being Point of T for l1 being Path of [s1,t1],[s2,t2] for l2 being Path of [s2,t2],[s3,t3] for p1 being Path of s1,s2 for p2 being Path of s2,s3 st [s1,t1],[s2,t2] are_connected & [s2,t2],[s3,t3] are_connected & p1 = pr1 l1 & p2 = pr1 l2 holds pr1 (l1 + l2) = p1 + p2 proof let S, T be non empty TopSpace; ::_thesis: for s1, s2, s3 being Point of S for t1, t2, t3 being Point of T for l1 being Path of [s1,t1],[s2,t2] for l2 being Path of [s2,t2],[s3,t3] for p1 being Path of s1,s2 for p2 being Path of s2,s3 st [s1,t1],[s2,t2] are_connected & [s2,t2],[s3,t3] are_connected & p1 = pr1 l1 & p2 = pr1 l2 holds pr1 (l1 + l2) = p1 + p2 let s1, s2, s3 be Point of S; ::_thesis: for t1, t2, t3 being Point of T for l1 being Path of [s1,t1],[s2,t2] for l2 being Path of [s2,t2],[s3,t3] for p1 being Path of s1,s2 for p2 being Path of s2,s3 st [s1,t1],[s2,t2] are_connected & [s2,t2],[s3,t3] are_connected & p1 = pr1 l1 & p2 = pr1 l2 holds pr1 (l1 + l2) = p1 + p2 let t1, t2, t3 be Point of T; ::_thesis: for l1 being Path of [s1,t1],[s2,t2] for l2 being Path of [s2,t2],[s3,t3] for p1 being Path of s1,s2 for p2 being Path of s2,s3 st [s1,t1],[s2,t2] are_connected & [s2,t2],[s3,t3] are_connected & p1 = pr1 l1 & p2 = pr1 l2 holds pr1 (l1 + l2) = p1 + p2 let l1 be Path of [s1,t1],[s2,t2]; ::_thesis: for l2 being Path of [s2,t2],[s3,t3] for p1 being Path of s1,s2 for p2 being Path of s2,s3 st [s1,t1],[s2,t2] are_connected & [s2,t2],[s3,t3] are_connected & p1 = pr1 l1 & p2 = pr1 l2 holds pr1 (l1 + l2) = p1 + p2 let l2 be Path of [s2,t2],[s3,t3]; ::_thesis: for p1 being Path of s1,s2 for p2 being Path of s2,s3 st [s1,t1],[s2,t2] are_connected & [s2,t2],[s3,t3] are_connected & p1 = pr1 l1 & p2 = pr1 l2 holds pr1 (l1 + l2) = p1 + p2 let p1 be Path of s1,s2; ::_thesis: for p2 being Path of s2,s3 st [s1,t1],[s2,t2] are_connected & [s2,t2],[s3,t3] are_connected & p1 = pr1 l1 & p2 = pr1 l2 holds pr1 (l1 + l2) = p1 + p2 let p2 be Path of s2,s3; ::_thesis: ( [s1,t1],[s2,t2] are_connected & [s2,t2],[s3,t3] are_connected & p1 = pr1 l1 & p2 = pr1 l2 implies pr1 (l1 + l2) = p1 + p2 ) assume that A1: ( [s1,t1],[s2,t2] are_connected & [s2,t2],[s3,t3] are_connected ) and A2: p1 = pr1 l1 and A3: p2 = pr1 l2 ; ::_thesis: pr1 (l1 + l2) = p1 + p2 A4: ( s1,s2 are_connected & s2,s3 are_connected ) by A1, Th11; now__::_thesis:_for_x_being_Element_of_I[01]_holds_(pr1_(l1_+_l2))_._x_=_(p1_+_p2)_._x A5: dom l2 = the carrier of I[01] by FUNCT_2:def_1; A6: dom l1 = the carrier of I[01] by FUNCT_2:def_1; let x be Element of I[01]; ::_thesis: (pr1 (l1 + l2)) . b1 = (p1 + p2) . b1 A7: dom (l1 + l2) = the carrier of I[01] by FUNCT_2:def_1; percases ( x <= 1 / 2 or x >= 1 / 2 ) ; supposeA8: x <= 1 / 2 ; ::_thesis: (pr1 (l1 + l2)) . b1 = (p1 + p2) . b1 then A9: 2 * x is Point of I[01] by BORSUK_6:3; thus (pr1 (l1 + l2)) . x = ((l1 + l2) . x) `1 by A7, MCART_1:def_12 .= (l1 . (2 * x)) `1 by A1, A8, BORSUK_2:def_5 .= p1 . (2 * x) by A2, A6, A9, MCART_1:def_12 .= (p1 + p2) . x by A4, A8, BORSUK_2:def_5 ; ::_thesis: verum end; supposeA10: x >= 1 / 2 ; ::_thesis: (pr1 (l1 + l2)) . b1 = (p1 + p2) . b1 then A11: (2 * x) - 1 is Point of I[01] by BORSUK_6:4; thus (pr1 (l1 + l2)) . x = ((l1 + l2) . x) `1 by A7, MCART_1:def_12 .= (l2 . ((2 * x) - 1)) `1 by A1, A10, BORSUK_2:def_5 .= p2 . ((2 * x) - 1) by A3, A5, A11, MCART_1:def_12 .= (p1 + p2) . x by A4, A10, BORSUK_2:def_5 ; ::_thesis: verum end; end; end; hence pr1 (l1 + l2) = p1 + p2 by FUNCT_2:63; ::_thesis: verum end; theorem :: TOPALG_4:24 for S, T being non empty pathwise_connected TopSpace for s1, s2, s3 being Point of S for t1, t2, t3 being Point of T for l1 being Path of [s1,t1],[s2,t2] for l2 being Path of [s2,t2],[s3,t3] holds pr1 (l1 + l2) = (pr1 l1) + (pr1 l2) proof let S, T be non empty pathwise_connected TopSpace; ::_thesis: for s1, s2, s3 being Point of S for t1, t2, t3 being Point of T for l1 being Path of [s1,t1],[s2,t2] for l2 being Path of [s2,t2],[s3,t3] holds pr1 (l1 + l2) = (pr1 l1) + (pr1 l2) let s1, s2, s3 be Point of S; ::_thesis: for t1, t2, t3 being Point of T for l1 being Path of [s1,t1],[s2,t2] for l2 being Path of [s2,t2],[s3,t3] holds pr1 (l1 + l2) = (pr1 l1) + (pr1 l2) let t1, t2, t3 be Point of T; ::_thesis: for l1 being Path of [s1,t1],[s2,t2] for l2 being Path of [s2,t2],[s3,t3] holds pr1 (l1 + l2) = (pr1 l1) + (pr1 l2) let l1 be Path of [s1,t1],[s2,t2]; ::_thesis: for l2 being Path of [s2,t2],[s3,t3] holds pr1 (l1 + l2) = (pr1 l1) + (pr1 l2) let l2 be Path of [s2,t2],[s3,t3]; ::_thesis: pr1 (l1 + l2) = (pr1 l1) + (pr1 l2) ( [s1,t1],[s2,t2] are_connected & [s2,t2],[s3,t3] are_connected ) by BORSUK_2:def_3; hence pr1 (l1 + l2) = (pr1 l1) + (pr1 l2) by Th23; ::_thesis: verum end; theorem Th25: :: TOPALG_4:25 for S, T being non empty TopSpace for s1, s2, s3 being Point of S for t1, t2, t3 being Point of T for l1 being Path of [s1,t1],[s2,t2] for l2 being Path of [s2,t2],[s3,t3] for p1 being Path of t1,t2 for p2 being Path of t2,t3 st [s1,t1],[s2,t2] are_connected & [s2,t2],[s3,t3] are_connected & p1 = pr2 l1 & p2 = pr2 l2 holds pr2 (l1 + l2) = p1 + p2 proof let S, T be non empty TopSpace; ::_thesis: for s1, s2, s3 being Point of S for t1, t2, t3 being Point of T for l1 being Path of [s1,t1],[s2,t2] for l2 being Path of [s2,t2],[s3,t3] for p1 being Path of t1,t2 for p2 being Path of t2,t3 st [s1,t1],[s2,t2] are_connected & [s2,t2],[s3,t3] are_connected & p1 = pr2 l1 & p2 = pr2 l2 holds pr2 (l1 + l2) = p1 + p2 let s1, s2, s3 be Point of S; ::_thesis: for t1, t2, t3 being Point of T for l1 being Path of [s1,t1],[s2,t2] for l2 being Path of [s2,t2],[s3,t3] for p1 being Path of t1,t2 for p2 being Path of t2,t3 st [s1,t1],[s2,t2] are_connected & [s2,t2],[s3,t3] are_connected & p1 = pr2 l1 & p2 = pr2 l2 holds pr2 (l1 + l2) = p1 + p2 let t1, t2, t3 be Point of T; ::_thesis: for l1 being Path of [s1,t1],[s2,t2] for l2 being Path of [s2,t2],[s3,t3] for p1 being Path of t1,t2 for p2 being Path of t2,t3 st [s1,t1],[s2,t2] are_connected & [s2,t2],[s3,t3] are_connected & p1 = pr2 l1 & p2 = pr2 l2 holds pr2 (l1 + l2) = p1 + p2 let l1 be Path of [s1,t1],[s2,t2]; ::_thesis: for l2 being Path of [s2,t2],[s3,t3] for p1 being Path of t1,t2 for p2 being Path of t2,t3 st [s1,t1],[s2,t2] are_connected & [s2,t2],[s3,t3] are_connected & p1 = pr2 l1 & p2 = pr2 l2 holds pr2 (l1 + l2) = p1 + p2 let l2 be Path of [s2,t2],[s3,t3]; ::_thesis: for p1 being Path of t1,t2 for p2 being Path of t2,t3 st [s1,t1],[s2,t2] are_connected & [s2,t2],[s3,t3] are_connected & p1 = pr2 l1 & p2 = pr2 l2 holds pr2 (l1 + l2) = p1 + p2 let p1 be Path of t1,t2; ::_thesis: for p2 being Path of t2,t3 st [s1,t1],[s2,t2] are_connected & [s2,t2],[s3,t3] are_connected & p1 = pr2 l1 & p2 = pr2 l2 holds pr2 (l1 + l2) = p1 + p2 let p2 be Path of t2,t3; ::_thesis: ( [s1,t1],[s2,t2] are_connected & [s2,t2],[s3,t3] are_connected & p1 = pr2 l1 & p2 = pr2 l2 implies pr2 (l1 + l2) = p1 + p2 ) assume that A1: ( [s1,t1],[s2,t2] are_connected & [s2,t2],[s3,t3] are_connected ) and A2: p1 = pr2 l1 and A3: p2 = pr2 l2 ; ::_thesis: pr2 (l1 + l2) = p1 + p2 A4: ( t1,t2 are_connected & t2,t3 are_connected ) by A1, Th12; now__::_thesis:_for_x_being_Element_of_I[01]_holds_(pr2_(l1_+_l2))_._x_=_(p1_+_p2)_._x A5: dom l2 = the carrier of I[01] by FUNCT_2:def_1; A6: dom l1 = the carrier of I[01] by FUNCT_2:def_1; let x be Element of I[01]; ::_thesis: (pr2 (l1 + l2)) . b1 = (p1 + p2) . b1 A7: dom (l1 + l2) = the carrier of I[01] by FUNCT_2:def_1; percases ( x <= 1 / 2 or x >= 1 / 2 ) ; supposeA8: x <= 1 / 2 ; ::_thesis: (pr2 (l1 + l2)) . b1 = (p1 + p2) . b1 then A9: 2 * x is Point of I[01] by BORSUK_6:3; thus (pr2 (l1 + l2)) . x = ((l1 + l2) . x) `2 by A7, MCART_1:def_13 .= (l1 . (2 * x)) `2 by A1, A8, BORSUK_2:def_5 .= p1 . (2 * x) by A2, A6, A9, MCART_1:def_13 .= (p1 + p2) . x by A4, A8, BORSUK_2:def_5 ; ::_thesis: verum end; supposeA10: x >= 1 / 2 ; ::_thesis: (pr2 (l1 + l2)) . b1 = (p1 + p2) . b1 then A11: (2 * x) - 1 is Point of I[01] by BORSUK_6:4; thus (pr2 (l1 + l2)) . x = ((l1 + l2) . x) `2 by A7, MCART_1:def_13 .= (l2 . ((2 * x) - 1)) `2 by A1, A10, BORSUK_2:def_5 .= p2 . ((2 * x) - 1) by A3, A5, A11, MCART_1:def_13 .= (p1 + p2) . x by A4, A10, BORSUK_2:def_5 ; ::_thesis: verum end; end; end; hence pr2 (l1 + l2) = p1 + p2 by FUNCT_2:63; ::_thesis: verum end; theorem :: TOPALG_4:26 for S, T being non empty pathwise_connected TopSpace for s1, s2, s3 being Point of S for t1, t2, t3 being Point of T for l1 being Path of [s1,t1],[s2,t2] for l2 being Path of [s2,t2],[s3,t3] holds pr2 (l1 + l2) = (pr2 l1) + (pr2 l2) proof let S, T be non empty pathwise_connected TopSpace; ::_thesis: for s1, s2, s3 being Point of S for t1, t2, t3 being Point of T for l1 being Path of [s1,t1],[s2,t2] for l2 being Path of [s2,t2],[s3,t3] holds pr2 (l1 + l2) = (pr2 l1) + (pr2 l2) let s1, s2, s3 be Point of S; ::_thesis: for t1, t2, t3 being Point of T for l1 being Path of [s1,t1],[s2,t2] for l2 being Path of [s2,t2],[s3,t3] holds pr2 (l1 + l2) = (pr2 l1) + (pr2 l2) let t1, t2, t3 be Point of T; ::_thesis: for l1 being Path of [s1,t1],[s2,t2] for l2 being Path of [s2,t2],[s3,t3] holds pr2 (l1 + l2) = (pr2 l1) + (pr2 l2) let l1 be Path of [s1,t1],[s2,t2]; ::_thesis: for l2 being Path of [s2,t2],[s3,t3] holds pr2 (l1 + l2) = (pr2 l1) + (pr2 l2) let l2 be Path of [s2,t2],[s3,t3]; ::_thesis: pr2 (l1 + l2) = (pr2 l1) + (pr2 l2) ( [s1,t1],[s2,t2] are_connected & [s2,t2],[s3,t3] are_connected ) by BORSUK_2:def_3; hence pr2 (l1 + l2) = (pr2 l1) + (pr2 l2) by Th25; ::_thesis: verum end; definition let S, T be non empty TopSpace; let s be Point of S; let t be Point of T; set pS = pi_1 ([:S,T:],[s,t]); set G = <*(pi_1 (S,s)),(pi_1 (T,t))*>; set pT = product <*(pi_1 (S,s)),(pi_1 (T,t))*>; func FGPrIso (s,t) -> Function of (pi_1 ([:S,T:],[s,t])),(product <*(pi_1 (S,s)),(pi_1 (T,t))*>) means :Def2: :: TOPALG_4:def 2 for x being Point of (pi_1 ([:S,T:],[s,t])) ex l being Loop of [s,t] st ( x = Class ((EqRel ([:S,T:],[s,t])),l) & it . x = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> ); existence ex b1 being Function of (pi_1 ([:S,T:],[s,t])),(product <*(pi_1 (S,s)),(pi_1 (T,t))*>) st for x being Point of (pi_1 ([:S,T:],[s,t])) ex l being Loop of [s,t] st ( x = Class ((EqRel ([:S,T:],[s,t])),l) & b1 . x = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> ) proof defpred S1[ set , set ] means ex l being Loop of [s,t] st ( \$1 = Class ((EqRel ([:S,T:],[s,t])),l) & \$2 = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> ); A1: for x being Element of (pi_1 ([:S,T:],[s,t])) ex y being Element of (product <*(pi_1 (S,s)),(pi_1 (T,t))*>) st S1[x,y] proof let x be Element of (pi_1 ([:S,T:],[s,t])); ::_thesis: ex y being Element of (product <*(pi_1 (S,s)),(pi_1 (T,t))*>) st S1[x,y] consider l being Loop of [s,t] such that A2: x = Class ((EqRel ([:S,T:],[s,t])),l) by TOPALG_1:47; set B = Class ((EqRel (T,t)),(pr2 l)); set A = Class ((EqRel (S,s)),(pr1 l)); A3: dom (Carrier <*(pi_1 (S,s)),(pi_1 (T,t))*>) = {1,2} by PARTFUN1:def_2; A4: now__::_thesis:_for_x_being_set_st_x_in_dom_(Carrier_<*(pi_1_(S,s)),(pi_1_(T,t))*>)_holds_ <*(Class_((EqRel_(S,s)),(pr1_l))),(Class_((EqRel_(T,t)),(pr2_l)))*>_._x_in_(Carrier_<*(pi_1_(S,s)),(pi_1_(T,t))*>)_._x let x be set ; ::_thesis: ( x in dom (Carrier <*(pi_1 (S,s)),(pi_1 (T,t))*>) implies <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> . x in (Carrier <*(pi_1 (S,s)),(pi_1 (T,t))*>) . x ) assume A5: x in dom (Carrier <*(pi_1 (S,s)),(pi_1 (T,t))*>) ; ::_thesis: <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> . x in (Carrier <*(pi_1 (S,s)),(pi_1 (T,t))*>) . x A6: ( x = 1 or x = 2 ) by A5, TARSKI:def_2; A7: ( <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> . 1 = Class ((EqRel (S,s)),(pr1 l)) & <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> . 2 = Class ((EqRel (T,t)),(pr2 l)) ) by FINSEQ_1:44; A8: ( <*(pi_1 (S,s)),(pi_1 (T,t))*> . 1 = pi_1 (S,s) & <*(pi_1 (S,s)),(pi_1 (T,t))*> . 2 = pi_1 (T,t) ) by FINSEQ_1:44; ex R being 1-sorted st ( R = <*(pi_1 (S,s)),(pi_1 (T,t))*> . x & (Carrier <*(pi_1 (S,s)),(pi_1 (T,t))*>) . x = the carrier of R ) by A5, PRALG_1:def_13; hence <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> . x in (Carrier <*(pi_1 (S,s)),(pi_1 (T,t))*>) . x by A8, A7, A6, TOPALG_1:47; ::_thesis: verum end; ( the carrier of (product <*(pi_1 (S,s)),(pi_1 (T,t))*>) = product (Carrier <*(pi_1 (S,s)),(pi_1 (T,t))*>) & dom <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> = {1,2} ) by FINSEQ_1:2, FINSEQ_1:89, GROUP_7:def_2; then reconsider y = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> as Element of (product <*(pi_1 (S,s)),(pi_1 (T,t))*>) by A3, A4, CARD_3:9; take y ; ::_thesis: S1[x,y] take l ; ::_thesis: ( x = Class ((EqRel ([:S,T:],[s,t])),l) & y = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> ) thus ( x = Class ((EqRel ([:S,T:],[s,t])),l) & y = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> ) by A2; ::_thesis: verum end; ex h being Function of (pi_1 ([:S,T:],[s,t])),(product <*(pi_1 (S,s)),(pi_1 (T,t))*>) st for x being Element of (pi_1 ([:S,T:],[s,t])) holds S1[x,h . x] from FUNCT_2:sch_3(A1); hence ex b1 being Function of (pi_1 ([:S,T:],[s,t])),(product <*(pi_1 (S,s)),(pi_1 (T,t))*>) st for x being Point of (pi_1 ([:S,T:],[s,t])) ex l being Loop of [s,t] st ( x = Class ((EqRel ([:S,T:],[s,t])),l) & b1 . x = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> ) ; ::_thesis: verum end; uniqueness for b1, b2 being Function of (pi_1 ([:S,T:],[s,t])),(product <*(pi_1 (S,s)),(pi_1 (T,t))*>) st ( for x being Point of (pi_1 ([:S,T:],[s,t])) ex l being Loop of [s,t] st ( x = Class ((EqRel ([:S,T:],[s,t])),l) & b1 . x = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> ) ) & ( for x being Point of (pi_1 ([:S,T:],[s,t])) ex l being Loop of [s,t] st ( x = Class ((EqRel ([:S,T:],[s,t])),l) & b2 . x = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> ) ) holds b1 = b2 proof let f, g be Function of (pi_1 ([:S,T:],[s,t])),(product <*(pi_1 (S,s)),(pi_1 (T,t))*>); ::_thesis: ( ( for x being Point of (pi_1 ([:S,T:],[s,t])) ex l being Loop of [s,t] st ( x = Class ((EqRel ([:S,T:],[s,t])),l) & f . x = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> ) ) & ( for x being Point of (pi_1 ([:S,T:],[s,t])) ex l being Loop of [s,t] st ( x = Class ((EqRel ([:S,T:],[s,t])),l) & g . x = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> ) ) implies f = g ) assume that A9: for x being Point of (pi_1 ([:S,T:],[s,t])) ex l being Loop of [s,t] st ( x = Class ((EqRel ([:S,T:],[s,t])),l) & f . x = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> ) and A10: for x being Point of (pi_1 ([:S,T:],[s,t])) ex l being Loop of [s,t] st ( x = Class ((EqRel ([:S,T:],[s,t])),l) & g . x = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> ) ; ::_thesis: f = g now__::_thesis:_for_x_being_Point_of_(pi_1_([:S,T:],[s,t]))_holds_f_._x_=_g_._x let x be Point of (pi_1 ([:S,T:],[s,t])); ::_thesis: f . x = g . x consider l1 being Loop of [s,t] such that A11: x = Class ((EqRel ([:S,T:],[s,t])),l1) and A12: f . x = <*(Class ((EqRel (S,s)),(pr1 l1))),(Class ((EqRel (T,t)),(pr2 l1)))*> by A9; consider l2 being Loop of [s,t] such that A13: x = Class ((EqRel ([:S,T:],[s,t])),l2) and A14: g . x = <*(Class ((EqRel (S,s)),(pr1 l2))),(Class ((EqRel (T,t)),(pr2 l2)))*> by A10; A15: l1,l2 are_homotopic by A11, A13, TOPALG_1:46; then pr2 l1, pr2 l2 are_homotopic by Th20; then A16: Class ((EqRel (T,t)),(pr2 l1)) = Class ((EqRel (T,t)),(pr2 l2)) by TOPALG_1:46; pr1 l1, pr1 l2 are_homotopic by A15, Th19; hence f . x = g . x by A12, A14, A16, TOPALG_1:46; ::_thesis: verum end; hence f = g by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def2 defines FGPrIso TOPALG_4:def_2_:_ for S, T being non empty TopSpace for s being Point of S for t being Point of T for b5 being Function of (pi_1 ([:S,T:],[s,t])),(product <*(pi_1 (S,s)),(pi_1 (T,t))*>) holds ( b5 = FGPrIso (s,t) iff for x being Point of (pi_1 ([:S,T:],[s,t])) ex l being Loop of [s,t] st ( x = Class ((EqRel ([:S,T:],[s,t])),l) & b5 . x = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> ) ); theorem Th27: :: TOPALG_4:27 for S, T being non empty TopSpace for s being Point of S for t being Point of T for x being Point of (pi_1 ([:S,T:],[s,t])) for l being Loop of [s,t] st x = Class ((EqRel ([:S,T:],[s,t])),l) holds (FGPrIso (s,t)) . x = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> proof let S, T be non empty TopSpace; ::_thesis: for s being Point of S for t being Point of T for x being Point of (pi_1 ([:S,T:],[s,t])) for l being Loop of [s,t] st x = Class ((EqRel ([:S,T:],[s,t])),l) holds (FGPrIso (s,t)) . x = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> let s be Point of S; ::_thesis: for t being Point of T for x being Point of (pi_1 ([:S,T:],[s,t])) for l being Loop of [s,t] st x = Class ((EqRel ([:S,T:],[s,t])),l) holds (FGPrIso (s,t)) . x = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> let t be Point of T; ::_thesis: for x being Point of (pi_1 ([:S,T:],[s,t])) for l being Loop of [s,t] st x = Class ((EqRel ([:S,T:],[s,t])),l) holds (FGPrIso (s,t)) . x = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> let x be Point of (pi_1 ([:S,T:],[s,t])); ::_thesis: for l being Loop of [s,t] st x = Class ((EqRel ([:S,T:],[s,t])),l) holds (FGPrIso (s,t)) . x = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> let l be Loop of [s,t]; ::_thesis: ( x = Class ((EqRel ([:S,T:],[s,t])),l) implies (FGPrIso (s,t)) . x = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> ) consider l1 being Loop of [s,t] such that A1: x = Class ((EqRel ([:S,T:],[s,t])),l1) and A2: (FGPrIso (s,t)) . x = <*(Class ((EqRel (S,s)),(pr1 l1))),(Class ((EqRel (T,t)),(pr2 l1)))*> by Def2; assume x = Class ((EqRel ([:S,T:],[s,t])),l) ; ::_thesis: (FGPrIso (s,t)) . x = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> then A3: l,l1 are_homotopic by A1, TOPALG_1:46; then pr2 l, pr2 l1 are_homotopic by Th20; then A4: Class ((EqRel (T,t)),(pr2 l)) = Class ((EqRel (T,t)),(pr2 l1)) by TOPALG_1:46; pr1 l, pr1 l1 are_homotopic by A3, Th19; hence (FGPrIso (s,t)) . x = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> by A2, A4, TOPALG_1:46; ::_thesis: verum end; theorem Th28: :: TOPALG_4:28 for S, T being non empty TopSpace for s being Point of S for t being Point of T for l being Loop of [s,t] holds (FGPrIso (s,t)) . (Class ((EqRel ([:S,T:],[s,t])),l)) = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> proof let S, T be non empty TopSpace; ::_thesis: for s being Point of S for t being Point of T for l being Loop of [s,t] holds (FGPrIso (s,t)) . (Class ((EqRel ([:S,T:],[s,t])),l)) = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> let s be Point of S; ::_thesis: for t being Point of T for l being Loop of [s,t] holds (FGPrIso (s,t)) . (Class ((EqRel ([:S,T:],[s,t])),l)) = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> let t be Point of T; ::_thesis: for l being Loop of [s,t] holds (FGPrIso (s,t)) . (Class ((EqRel ([:S,T:],[s,t])),l)) = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> let l be Loop of [s,t]; ::_thesis: (FGPrIso (s,t)) . (Class ((EqRel ([:S,T:],[s,t])),l)) = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> Class ((EqRel ([:S,T:],[s,t])),l) is Point of (pi_1 ([:S,T:],[s,t])) by TOPALG_1:47; hence (FGPrIso (s,t)) . (Class ((EqRel ([:S,T:],[s,t])),l)) = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> by Th27; ::_thesis: verum end; registration let S, T be non empty TopSpace; let s be Point of S; let t be Point of T; cluster FGPrIso (s,t) -> one-to-one onto ; coherence ( FGPrIso (s,t) is one-to-one & FGPrIso (s,t) is onto ) proof set F = FGPrIso (s,t); set G = <*(pi_1 (S,s)),(pi_1 (T,t))*>; set pS = pi_1 ([:S,T:],[s,t]); set pT = product <*(pi_1 (S,s)),(pi_1 (T,t))*>; A1: the carrier of (product <*(pi_1 (S,s)),(pi_1 (T,t))*>) = product (Carrier <*(pi_1 (S,s)),(pi_1 (T,t))*>) by GROUP_7:def_2; thus FGPrIso (s,t) is one-to-one ::_thesis: FGPrIso (s,t) is onto proof let a, b be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not a in proj1 (FGPrIso (s,t)) or not b in proj1 (FGPrIso (s,t)) or not (FGPrIso (s,t)) . a = (FGPrIso (s,t)) . b or a = b ) assume a in dom (FGPrIso (s,t)) ; ::_thesis: ( not b in proj1 (FGPrIso (s,t)) or not (FGPrIso (s,t)) . a = (FGPrIso (s,t)) . b or a = b ) then consider la being Loop of [s,t] such that A2: a = Class ((EqRel ([:S,T:],[s,t])),la) and A3: (FGPrIso (s,t)) . a = <*(Class ((EqRel (S,s)),(pr1 la))),(Class ((EqRel (T,t)),(pr2 la)))*> by Def2; assume b in dom (FGPrIso (s,t)) ; ::_thesis: ( not (FGPrIso (s,t)) . a = (FGPrIso (s,t)) . b or a = b ) then consider lb being Loop of [s,t] such that A4: b = Class ((EqRel ([:S,T:],[s,t])),lb) and A5: (FGPrIso (s,t)) . b = <*(Class ((EqRel (S,s)),(pr1 lb))),(Class ((EqRel (T,t)),(pr2 lb)))*> by Def2; assume A6: (FGPrIso (s,t)) . a = (FGPrIso (s,t)) . b ; ::_thesis: a = b then Class ((EqRel (T,t)),(pr2 la)) = Class ((EqRel (T,t)),(pr2 lb)) by A3, A5, FINSEQ_1:77; then A7: pr2 la, pr2 lb are_homotopic by TOPALG_1:46; Class ((EqRel (S,s)),(pr1 la)) = Class ((EqRel (S,s)),(pr1 lb)) by A3, A5, A6, FINSEQ_1:77; then pr1 la, pr1 lb are_homotopic by TOPALG_1:46; then la,lb are_homotopic by A7, Th22; hence a = b by A2, A4, TOPALG_1:46; ::_thesis: verum end; thus rng (FGPrIso (s,t)) c= the carrier of (product <*(pi_1 (S,s)),(pi_1 (T,t))*>) ; :: according to XBOOLE_0:def_10,FUNCT_2:def_3 ::_thesis: the carrier of (product <*(pi_1 (S,s)),(pi_1 (T,t))*>) c= rng (FGPrIso (s,t)) let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in the carrier of (product <*(pi_1 (S,s)),(pi_1 (T,t))*>) or y in rng (FGPrIso (s,t)) ) assume y in the carrier of (product <*(pi_1 (S,s)),(pi_1 (T,t))*>) ; ::_thesis: y in rng (FGPrIso (s,t)) then consider g being Function such that A8: y = g and A9: dom g = dom (Carrier <*(pi_1 (S,s)),(pi_1 (T,t))*>) and A10: for z being set st z in dom (Carrier <*(pi_1 (S,s)),(pi_1 (T,t))*>) holds g . z in (Carrier <*(pi_1 (S,s)),(pi_1 (T,t))*>) . z by A1, CARD_3:def_5; A11: dom (Carrier <*(pi_1 (S,s)),(pi_1 (T,t))*>) = {1,2} by PARTFUN1:def_2; then reconsider g = g as FinSequence by A9, FINSEQ_1:2, FINSEQ_1:def_2; A12: len g = 2 by A9, A11, FINSEQ_1:2, FINSEQ_1:def_3; A13: ( ex R2 being 1-sorted st ( R2 = <*(pi_1 (S,s)),(pi_1 (T,t))*> . 2 & (Carrier <*(pi_1 (S,s)),(pi_1 (T,t))*>) . 2 = the carrier of R2 ) & <*(pi_1 (S,s)),(pi_1 (T,t))*> . 2 = pi_1 (T,t) ) by Lm2, FINSEQ_1:44, PRALG_1:def_13; g . 2 in (Carrier <*(pi_1 (S,s)),(pi_1 (T,t))*>) . 2 by A10, A11, Lm2; then consider l2 being Loop of t such that A14: g . 2 = Class ((EqRel (T,t)),l2) by A13, TOPALG_1:47; A15: ( ex R1 being 1-sorted st ( R1 = <*(pi_1 (S,s)),(pi_1 (T,t))*> . 1 & (Carrier <*(pi_1 (S,s)),(pi_1 (T,t))*>) . 1 = the carrier of R1 ) & <*(pi_1 (S,s)),(pi_1 (T,t))*> . 1 = pi_1 (S,s) ) by Lm1, FINSEQ_1:44, PRALG_1:def_13; g . 1 in (Carrier <*(pi_1 (S,s)),(pi_1 (T,t))*>) . 1 by A10, A11, Lm1; then consider l1 being Loop of s such that A16: g . 1 = Class ((EqRel (S,s)),l1) by A15, TOPALG_1:47; set x = Class ((EqRel ([:S,T:],[s,t])),<:l1,l2:>); A17: dom l1 = the carrier of I[01] by FUNCT_2:def_1 .= dom l2 by FUNCT_2:def_1 ; dom (FGPrIso (s,t)) = the carrier of (pi_1 ([:S,T:],[s,t])) by FUNCT_2:def_1; then A18: Class ((EqRel ([:S,T:],[s,t])),<:l1,l2:>) in dom (FGPrIso (s,t)) by TOPALG_1:47; (FGPrIso (s,t)) . (Class ((EqRel ([:S,T:],[s,t])),<:l1,l2:>)) = <*(Class ((EqRel (S,s)),(pr1 <:l1,l2:>))),(Class ((EqRel (T,t)),(pr2 <:l1,l2:>)))*> by Th28 .= <*(Class ((EqRel (S,s)),l1)),(Class ((EqRel (T,t)),(pr2 <:l1,l2:>)))*> by A17, Th7 .= <*(Class ((EqRel (S,s)),l1)),(Class ((EqRel (T,t)),l2))*> by A17, Th8 .= y by A8, A12, A16, A14, FINSEQ_1:44 ; hence y in rng (FGPrIso (s,t)) by A18, FUNCT_1:def_3; ::_thesis: verum end; end; registration let S, T be non empty TopSpace; let s be Point of S; let t be Point of T; cluster FGPrIso (s,t) -> multiplicative ; coherence FGPrIso (s,t) is multiplicative proof set F = FGPrIso (s,t); let a, b be Element of (pi_1 ([:S,T:],[s,t])); :: according to GROUP_6:def_6 ::_thesis: (FGPrIso (s,t)) . (a * b) = ((FGPrIso (s,t)) . a) * ((FGPrIso (s,t)) . b) consider la being Loop of [s,t] such that A1: a = Class ((EqRel ([:S,T:],[s,t])),la) and A2: (FGPrIso (s,t)) . a = <*(Class ((EqRel (S,s)),(pr1 la))),(Class ((EqRel (T,t)),(pr2 la)))*> by Def2; consider lb being Loop of [s,t] such that A3: b = Class ((EqRel ([:S,T:],[s,t])),lb) and A4: (FGPrIso (s,t)) . b = <*(Class ((EqRel (S,s)),(pr1 lb))),(Class ((EqRel (T,t)),(pr2 lb)))*> by Def2; reconsider B1 = Class ((EqRel (T,t)),(pr2 la)), B2 = Class ((EqRel (T,t)),(pr2 lb)) as Element of (pi_1 (T,t)) by TOPALG_1:47; reconsider A1 = Class ((EqRel (S,s)),(pr1 la)), A2 = Class ((EqRel (S,s)),(pr1 lb)) as Element of (pi_1 (S,s)) by TOPALG_1:47; consider lab being Loop of [s,t] such that A5: a * b = Class ((EqRel ([:S,T:],[s,t])),lab) and A6: (FGPrIso (s,t)) . (a * b) = <*(Class ((EqRel (S,s)),(pr1 lab))),(Class ((EqRel (T,t)),(pr2 lab)))*> by Def2; a * b = Class ((EqRel ([:S,T:],[s,t])),(la + lb)) by A1, A3, TOPALG_1:61; then A7: lab,la + lb are_homotopic by A5, TOPALG_1:46; then A8: pr1 lab, pr1 (la + lb) are_homotopic by Th19; A9: pr2 lab, pr2 (la + lb) are_homotopic by A7, Th20; A10: B1 * B2 = Class ((EqRel (T,t)),((pr2 la) + (pr2 lb))) by TOPALG_1:61 .= Class ((EqRel (T,t)),(pr2 (la + lb))) by Th25 .= Class ((EqRel (T,t)),(pr2 lab)) by A9, TOPALG_1:46 ; A1 * A2 = Class ((EqRel (S,s)),((pr1 la) + (pr1 lb))) by TOPALG_1:61 .= Class ((EqRel (S,s)),(pr1 (la + lb))) by Th23 .= Class ((EqRel (S,s)),(pr1 lab)) by A8, TOPALG_1:46 ; hence (FGPrIso (s,t)) . (a * b) = ((FGPrIso (s,t)) . a) * ((FGPrIso (s,t)) . b) by A2, A4, A6, A10, GROUP_7:29; ::_thesis: verum end; end; theorem Th29: :: TOPALG_4:29 for S, T being non empty TopSpace for s being Point of S for t being Point of T holds FGPrIso (s,t) is bijective proof let S, T be non empty TopSpace; ::_thesis: for s being Point of S for t being Point of T holds FGPrIso (s,t) is bijective let s be Point of S; ::_thesis: for t being Point of T holds FGPrIso (s,t) is bijective let t be Point of T; ::_thesis: FGPrIso (s,t) is bijective thus FGPrIso (s,t) is one-to-one ; :: according to FUNCT_2:def_4 ::_thesis: FGPrIso (s,t) is onto thus rng (FGPrIso (s,t)) = the carrier of (product <*(pi_1 (S,s)),(pi_1 (T,t))*>) by FUNCT_2:def_3; :: according to FUNCT_2:def_3 ::_thesis: verum end; theorem Th30: :: TOPALG_4:30 for S, T being non empty TopSpace for s being Point of S for t being Point of T holds pi_1 ([:S,T:],[s,t]), product <*(pi_1 (S,s)),(pi_1 (T,t))*> are_isomorphic proof let S, T be non empty TopSpace; ::_thesis: for s being Point of S for t being Point of T holds pi_1 ([:S,T:],[s,t]), product <*(pi_1 (S,s)),(pi_1 (T,t))*> are_isomorphic let s be Point of S; ::_thesis: for t being Point of T holds pi_1 ([:S,T:],[s,t]), product <*(pi_1 (S,s)),(pi_1 (T,t))*> are_isomorphic let t be Point of T; ::_thesis: pi_1 ([:S,T:],[s,t]), product <*(pi_1 (S,s)),(pi_1 (T,t))*> are_isomorphic take FGPrIso (s,t) ; :: according to GROUP_6:def_11 ::_thesis: FGPrIso (s,t) is bijective thus FGPrIso (s,t) is bijective by Th29; ::_thesis: verum end; theorem :: TOPALG_4:31 for S, T being non empty TopSpace for s1, s2 being Point of S for t1, t2 being Point of T for f being Homomorphism of (pi_1 (S,s1)),(pi_1 (S,s2)) for g being Homomorphism of (pi_1 (T,t1)),(pi_1 (T,t2)) st f is bijective & g is bijective holds (Gr2Iso (f,g)) * (FGPrIso (s1,t1)) is bijective proof let S, T be non empty TopSpace; ::_thesis: for s1, s2 being Point of S for t1, t2 being Point of T for f being Homomorphism of (pi_1 (S,s1)),(pi_1 (S,s2)) for g being Homomorphism of (pi_1 (T,t1)),(pi_1 (T,t2)) st f is bijective & g is bijective holds (Gr2Iso (f,g)) * (FGPrIso (s1,t1)) is bijective let s1, s2 be Point of S; ::_thesis: for t1, t2 being Point of T for f being Homomorphism of (pi_1 (S,s1)),(pi_1 (S,s2)) for g being Homomorphism of (pi_1 (T,t1)),(pi_1 (T,t2)) st f is bijective & g is bijective holds (Gr2Iso (f,g)) * (FGPrIso (s1,t1)) is bijective let t1, t2 be Point of T; ::_thesis: for f being Homomorphism of (pi_1 (S,s1)),(pi_1 (S,s2)) for g being Homomorphism of (pi_1 (T,t1)),(pi_1 (T,t2)) st f is bijective & g is bijective holds (Gr2Iso (f,g)) * (FGPrIso (s1,t1)) is bijective let f be Homomorphism of (pi_1 (S,s1)),(pi_1 (S,s2)); ::_thesis: for g being Homomorphism of (pi_1 (T,t1)),(pi_1 (T,t2)) st f is bijective & g is bijective holds (Gr2Iso (f,g)) * (FGPrIso (s1,t1)) is bijective let g be Homomorphism of (pi_1 (T,t1)),(pi_1 (T,t2)); ::_thesis: ( f is bijective & g is bijective implies (Gr2Iso (f,g)) * (FGPrIso (s1,t1)) is bijective ) assume ( f is bijective & g is bijective ) ; ::_thesis: (Gr2Iso (f,g)) * (FGPrIso (s1,t1)) is bijective then A1: Gr2Iso (f,g) is bijective by Th5; FGPrIso (s1,t1) is bijective by Th29; hence (Gr2Iso (f,g)) * (FGPrIso (s1,t1)) is bijective by A1, GROUP_6:64; ::_thesis: verum end; theorem :: TOPALG_4:32 for S, T being non empty pathwise_connected TopSpace for s1, s2 being Point of S for t1, t2 being Point of T holds pi_1 ([:S,T:],[s1,t1]), product <*(pi_1 (S,s2)),(pi_1 (T,t2))*> are_isomorphic proof let S, T be non empty pathwise_connected TopSpace; ::_thesis: for s1, s2 being Point of S for t1, t2 being Point of T holds pi_1 ([:S,T:],[s1,t1]), product <*(pi_1 (S,s2)),(pi_1 (T,t2))*> are_isomorphic let s1, s2 be Point of S; ::_thesis: for t1, t2 being Point of T holds pi_1 ([:S,T:],[s1,t1]), product <*(pi_1 (S,s2)),(pi_1 (T,t2))*> are_isomorphic let t1, t2 be Point of T; ::_thesis: pi_1 ([:S,T:],[s1,t1]), product <*(pi_1 (S,s2)),(pi_1 (T,t2))*> are_isomorphic ( pi_1 (S,s1), pi_1 (S,s2) are_isomorphic & pi_1 (T,t1), pi_1 (T,t2) are_isomorphic ) by TOPALG_3:33; then A1: product <*(pi_1 (S,s1)),(pi_1 (T,t1))*>, product <*(pi_1 (S,s2)),(pi_1 (T,t2))*> are_isomorphic by Th6; pi_1 ([:S,T:],[s1,t1]), product <*(pi_1 (S,s1)),(pi_1 (T,t1))*> are_isomorphic by Th30; hence pi_1 ([:S,T:],[s1,t1]), product <*(pi_1 (S,s2)),(pi_1 (T,t2))*> are_isomorphic by A1, GROUP_6:67; ::_thesis: verum end;