let X be non empty TopSpace; for x0, x1 being Point of X
for P being Path of x0,x1 st x0,x1 are_connected holds
pi_1-iso P is Homomorphism of (pi_1 (X,x1)),(pi_1 (X,x0))
let x0, x1 be Point of X; for P being Path of x0,x1 st x0,x1 are_connected holds
pi_1-iso P is Homomorphism of (pi_1 (X,x1)),(pi_1 (X,x0))
let P be Path of x0,x1; ( x0,x1 are_connected implies pi_1-iso P is Homomorphism of (pi_1 (X,x1)),(pi_1 (X,x0)) )
set f = pi_1-iso P;
assume A1:
x0,x1 are_connected
; pi_1-iso P is Homomorphism of (pi_1 (X,x1)),(pi_1 (X,x0))
now for x, y being Element of (pi_1 (X,x1)) holds (pi_1-iso P) . (x * y) = ((pi_1-iso P) . x) * ((pi_1-iso P) . y)let x,
y be
Element of
(pi_1 (X,x1));
(pi_1-iso P) . (x * y) = ((pi_1-iso P) . x) * ((pi_1-iso P) . y)consider A being
Loop of
x1 such that A2:
x = Class (
(EqRel (X,x1)),
A)
by Th47;
consider B being
Loop of
x1 such that A3:
y = Class (
(EqRel (X,x1)),
B)
by Th47;
consider D being
Loop of
x0 such that A4:
(pi_1-iso P) . y = Class (
(EqRel (X,x0)),
D)
by Th47;
(pi_1-iso P) . y = Class (
(EqRel (X,x0)),
((P + B) + (- P)))
by A1, A3, Def6;
then A5:
D,
(P + B) + (- P) are_homotopic
by A4, Th46;
A6:
(P + (A + B)) + (- P),
((P + A) + (- P)) + ((P + B) + (- P)) are_homotopic
by A1, Th43;
consider C being
Loop of
x0 such that A7:
(pi_1-iso P) . x = Class (
(EqRel (X,x0)),
C)
by Th47;
(pi_1-iso P) . x = Class (
(EqRel (X,x0)),
((P + A) + (- P)))
by A1, A2, Def6;
then
C,
(P + A) + (- P) are_homotopic
by A7, Th46;
then
C + D,
((P + A) + (- P)) + ((P + B) + (- P)) are_homotopic
by A5, BORSUK_6:75;
then A8:
(P + (A + B)) + (- P),
C + D are_homotopic
by A6, BORSUK_6:79;
thus (pi_1-iso P) . (x * y) =
(pi_1-iso P) . (Class ((EqRel (X,x1)),(A + B)))
by A2, A3, Lm4
.=
Class (
(EqRel (X,x0)),
((P + (A + B)) + (- P)))
by A1, Def6
.=
Class (
(EqRel (X,x0)),
(C + D))
by A8, Th46
.=
((pi_1-iso P) . x) * ((pi_1-iso P) . y)
by A7, A4, Lm4
;
verum end;
hence
pi_1-iso P is Homomorphism of (pi_1 (X,x1)),(pi_1 (X,x0))
by GROUP_6:def 6; verum