:: 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;