:: by Artur Korni{\l}owicz

::

:: Received August 20, 2004

:: Copyright (c) 2004-2018 Association of Mizar Users

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*>

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

ex b_{1} 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*> & b_{1} . x = <*(f . x1),(g . x2)*> )

for b_{1}, b_{2} 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*> & b_{1} . 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*> & b_{2} . x = <*(f . x1),(g . x2)*> ) ) holds

b_{1} = b_{2}

end;
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 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)*> );

ex b

for x being Element of (product <*G1,G2*>) ex x1 being Element of G1 ex x2 being Element of G2 st

( x = <*x1,x2*> & b

proof end;

uniqueness for b

( x = <*x1,x2*> & b

( x = <*x1,x2*> & b

b

proof 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 b_{7} being Function of (product <*G1,G2*>),(product <*H1,H2*>) holds

( b_{7} = 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*> & b_{7} . x = <*(f . x1),(g . x2)*> ) );

for G1, G2, H1, H2 being non empty multMagma

for f being Function of G1,H1

for g being Function of G2,H2

for b

( b

( x = <*x1,x2*> & b

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)*>

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

registration

let G1, G2, H1, H2 be Group;

let f be Homomorphism of G1,H1;

let g be Homomorphism of G2,H2;

coherence

Gr2Iso (f,g) is multiplicative

end;
let f be Homomorphism of G1,H1;

let g be Homomorphism of G2,H2;

coherence

Gr2Iso (f,g) is multiplicative

proof 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

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

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 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 by Th4, Th3;

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 by Th4, Th3;

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

product <*G1,G2*>, product <*H1,H2*> are_isomorphic

proof end;

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;

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

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

redefine func pr2 f -> Function of Y,T;

coherence

pr2 f is Function of Y,T

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

:: original: pr2redefine func pr2 f -> Function of Y,T;

coherence

pr2 f is Function of Y,T

proof end;

theorem Th9: :: TOPALG_4:9

for S, T, Y being non empty TopSpace

for f being continuous Function of Y,[:S,T:] holds pr1 f is continuous

for f being continuous Function of Y,[:S,T:] holds pr1 f is continuous

proof end;

theorem Th10: :: TOPALG_4:10

for S, T, Y being non empty TopSpace

for f being continuous Function of Y,[:S,T:] holds pr2 f is continuous

for f being continuous Function of Y,[:S,T:] holds pr2 f is continuous

proof 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

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

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

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

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

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 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]

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 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]

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

registration

let S, T be non empty pathwise_connected TopSpace;

coherence

[:S,T:] is pathwise_connected

end;
coherence

[:S,T:] is pathwise_connected

proof 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 by BORSUK_2:def 3, Th13;

:: original: pr2

redefine func pr2 L -> Path of t1,t2;

coherence

pr2 L is Path of t1,t2 by BORSUK_2:def 3, Th14;

end;
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 by BORSUK_2:def 3, Th13;

:: original: pr2

redefine func pr2 L -> Path of t1,t2;

coherence

pr2 L is Path of t1,t2 by BORSUK_2:def 3, Th14;

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

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

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

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

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

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

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

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

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 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)

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

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 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)

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 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))*>;

ex b_{1} 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) & b_{1} . x = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> )

for b_{1}, b_{2} 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) & b_{1} . 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) & b_{2} . x = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> ) ) holds

b_{1} = b_{2}

end;
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 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)))*> );

ex b

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) & b

proof end;

uniqueness for b

( x = Class ((EqRel ([:S,T:],[s,t])),l) & b

( x = Class ((EqRel ([:S,T:],[s,t])),l) & b

b

proof 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 b_{5} being Function of (pi_1 ([:S,T:],[s,t])),(product <*(pi_1 (S,s)),(pi_1 (T,t))*>) holds

( b_{5} = 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) & b_{5} . x = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> ) );

for S, T being non empty TopSpace

for s being Point of S

for t being Point of T

for b

( b

( x = Class ((EqRel ([:S,T:],[s,t])),l) & b

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)))*>

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 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)))*>

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

registration

let S, T be non empty TopSpace;

let s be Point of S;

let t be Point of T;

coherence

( FGPrIso (s,t) is one-to-one & FGPrIso (s,t) is onto )

end;
let s be Point of S;

let t be Point of T;

coherence

( FGPrIso (s,t) is one-to-one & FGPrIso (s,t) is onto )

proof end;

registration

let S, T be non empty TopSpace;

let s be Point of S;

let t be Point of T;

coherence

FGPrIso (s,t) is multiplicative

end;
let s be Point of S;

let t be Point of T;

coherence

FGPrIso (s,t) is multiplicative

proof end;

theorem :: TOPALG_4:29

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

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

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

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