let S, T be non empty TopSpace; :: thesis: for f being continuous Function of S,T

for a, b being Point of S

for P, Q being Path of a,b

for P1, Q1 being Path of f . a,f . b st P,Q are_homotopic & P1 = f * P & Q1 = f * Q holds

P1,Q1 are_homotopic

let f be continuous Function of S,T; :: thesis: for a, b being Point of S

for P, Q being Path of a,b

for P1, Q1 being Path of f . a,f . b st P,Q are_homotopic & P1 = f * P & Q1 = f * Q holds

P1,Q1 are_homotopic

let a, b be Point of S; :: thesis: for P, Q being Path of a,b

for P1, Q1 being Path of f . a,f . b st P,Q are_homotopic & P1 = f * P & Q1 = f * Q holds

P1,Q1 are_homotopic

let P, Q be Path of a,b; :: thesis: for P1, Q1 being Path of f . a,f . b st P,Q are_homotopic & P1 = f * P & Q1 = f * Q holds

P1,Q1 are_homotopic

let P1, Q1 be Path of f . a,f . b; :: thesis: ( P,Q are_homotopic & P1 = f * P & Q1 = f * Q implies P1,Q1 are_homotopic )

assume that

A1: P,Q are_homotopic and

A2: P1 = f * P and

A3: Q1 = f * Q ; :: thesis: P1,Q1 are_homotopic

set F = the Homotopy of P,Q;

take G = f * the Homotopy of P,Q; :: according to BORSUK_2:def 7 :: thesis: ( G is continuous & ( for b_{1} being Element of the carrier of K523() holds

( G . (b_{1},0) = P1 . b_{1} & G . (b_{1},1) = Q1 . b_{1} & G . (0,b_{1}) = f . a & G . (1,b_{1}) = f . b ) ) )

the Homotopy of P,Q is continuous by A1, BORSUK_6:def 11;

hence G is continuous ; :: thesis: for b_{1} being Element of the carrier of K523() holds

( G . (b_{1},0) = P1 . b_{1} & G . (b_{1},1) = Q1 . b_{1} & G . (0,b_{1}) = f . a & G . (1,b_{1}) = f . b )

let s be Point of I[01]; :: thesis: ( G . (s,0) = P1 . s & G . (s,1) = Q1 . s & G . (0,s) = f . a & G . (1,s) = f . b )

thus G . (s,0) = f . ( the Homotopy of P,Q . (s,j0)) by Lm1, BINOP_1:18

.= f . (P . s) by A1, BORSUK_6:def 11

.= P1 . s by A2, FUNCT_2:15 ; :: thesis: ( G . (s,1) = Q1 . s & G . (0,s) = f . a & G . (1,s) = f . b )

thus G . (s,1) = f . ( the Homotopy of P,Q . (s,j1)) by Lm1, BINOP_1:18

.= f . (Q . s) by A1, BORSUK_6:def 11

.= Q1 . s by A3, FUNCT_2:15 ; :: thesis: ( G . (0,s) = f . a & G . (1,s) = f . b )

thus G . (0,s) = f . ( the Homotopy of P,Q . (j0,s)) by Lm1, BINOP_1:18

.= f . a by A1, BORSUK_6:def 11 ; :: thesis: G . (1,s) = f . b

thus G . (1,s) = f . ( the Homotopy of P,Q . (j1,s)) by Lm1, BINOP_1:18

.= f . b by A1, BORSUK_6:def 11 ; :: thesis: verum

for a, b being Point of S

for P, Q being Path of a,b

for P1, Q1 being Path of f . a,f . b st P,Q are_homotopic & P1 = f * P & Q1 = f * Q holds

P1,Q1 are_homotopic

let f be continuous Function of S,T; :: thesis: for a, b being Point of S

for P, Q being Path of a,b

for P1, Q1 being Path of f . a,f . b st P,Q are_homotopic & P1 = f * P & Q1 = f * Q holds

P1,Q1 are_homotopic

let a, b be Point of S; :: thesis: for P, Q being Path of a,b

for P1, Q1 being Path of f . a,f . b st P,Q are_homotopic & P1 = f * P & Q1 = f * Q holds

P1,Q1 are_homotopic

let P, Q be Path of a,b; :: thesis: for P1, Q1 being Path of f . a,f . b st P,Q are_homotopic & P1 = f * P & Q1 = f * Q holds

P1,Q1 are_homotopic

let P1, Q1 be Path of f . a,f . b; :: thesis: ( P,Q are_homotopic & P1 = f * P & Q1 = f * Q implies P1,Q1 are_homotopic )

assume that

A1: P,Q are_homotopic and

A2: P1 = f * P and

A3: Q1 = f * Q ; :: thesis: P1,Q1 are_homotopic

set F = the Homotopy of P,Q;

take G = f * the Homotopy of P,Q; :: according to BORSUK_2:def 7 :: thesis: ( G is continuous & ( for b

( G . (b

the Homotopy of P,Q is continuous by A1, BORSUK_6:def 11;

hence G is continuous ; :: thesis: for b

( G . (b

let s be Point of I[01]; :: thesis: ( G . (s,0) = P1 . s & G . (s,1) = Q1 . s & G . (0,s) = f . a & G . (1,s) = f . b )

thus G . (s,0) = f . ( the Homotopy of P,Q . (s,j0)) by Lm1, BINOP_1:18

.= f . (P . s) by A1, BORSUK_6:def 11

.= P1 . s by A2, FUNCT_2:15 ; :: thesis: ( G . (s,1) = Q1 . s & G . (0,s) = f . a & G . (1,s) = f . b )

thus G . (s,1) = f . ( the Homotopy of P,Q . (s,j1)) by Lm1, BINOP_1:18

.= f . (Q . s) by A1, BORSUK_6:def 11

.= Q1 . s by A3, FUNCT_2:15 ; :: thesis: ( G . (0,s) = f . a & G . (1,s) = f . b )

thus G . (0,s) = f . ( the Homotopy of P,Q . (j0,s)) by Lm1, BINOP_1:18

.= f . a by A1, BORSUK_6:def 11 ; :: thesis: G . (1,s) = f . b

thus G . (1,s) = f . ( the Homotopy of P,Q . (j1,s)) by Lm1, BINOP_1:18

.= f . b by A1, BORSUK_6:def 11 ; :: thesis: verum