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
consider F being Homotopy of P,Q;
take G = f * F; :: according to BORSUK_2:def 7 :: thesis: ( G is continuous & ( for b₁ being Element of the carrier of K511() holds
( G . b₁,0 = P1 . b₁ & G . b₁,1 = Q1 . b₁ & G . 0 ,b₁ = f . a & G . 1,b₁ = f . b ) ) )
F is continuous by A1, BORSUK_6:def 13;
hence G is continuous ; :: thesis: for b₁ being Element of the carrier of K511() holds
( G . b₁,0 = P1 . b₁ & G . b₁,1 = Q1 . b₁ & G . 0 ,b₁ = f . a & G . 1,b₁ = 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 . (F . s,j0) by Lm1, BINOP_1:30
.= f . (P . s) by A1, BORSUK_6:def 13
.= P1 . s by A2, FUNCT_2:21 ; :: thesis: ( G . s,1 = Q1 . s & G . 0 ,s = f . a & G . 1,s = f . b )
thus G . s,1 = f . (F . s,j1) by Lm1, BINOP_1:30
.= f . (Q . s) by A1, BORSUK_6:def 13
.= Q1 . s by A3, FUNCT_2:21 ; :: thesis: ( G . 0 ,s = f . a & G . 1,s = f . b )
thus G . 0 ,s = f . (F . j0,s) by Lm1, BINOP_1:30
.= f . a by A1, BORSUK_6:def 13 ; :: thesis: G . 1,s = f . b
thus G . 1,s = f . (F . j1,s) by Lm1, BINOP_1:30
.= f . b by A1, BORSUK_6:def 13 ; :: thesis: verum