let S, T be non empty TopSpace; 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
for F being Homotopy of P,Q st P,Q are_homotopic & P1 = f * P & Q1 = f * Q holds
f * F is Homotopy of P1,Q1
let f be 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
for F being Homotopy of P,Q st P,Q are_homotopic & P1 = f * P & Q1 = f * Q holds
f * F is Homotopy of P1,Q1
let a, b be Point of S; for P, Q being Path of a,b
for P1, Q1 being Path of f . a,f . b
for F being Homotopy of P,Q st P,Q are_homotopic & P1 = f * P & Q1 = f * Q holds
f * F is Homotopy of P1,Q1
let P, Q be Path of a,b; for P1, Q1 being Path of f . a,f . b
for F being Homotopy of P,Q st P,Q are_homotopic & P1 = f * P & Q1 = f * Q holds
f * F is Homotopy of P1,Q1
let P1, Q1 be Path of f . a,f . b; for F being Homotopy of P,Q st P,Q are_homotopic & P1 = f * P & Q1 = f * Q holds
f * F is Homotopy of P1,Q1
let F be Homotopy of P,Q; ( P,Q are_homotopic & P1 = f * P & Q1 = f * Q implies f * F is Homotopy of P1,Q1 )
assume that
A1:
P,Q are_homotopic
and
A2:
P1 = f * P
and
A3:
Q1 = f * Q
; f * F is Homotopy of P1,Q1
thus
P1,Q1 are_homotopic
by A1, A2, A3, Th27; BORSUK_6:def 11 ( f * F is continuous & ( for b1 being Element of the carrier of K523() holds
( (f * F) . (b1,0) = P1 . b1 & (f * F) . (b1,1) = Q1 . b1 & (f * F) . (0,b1) = f . a & (f * F) . (1,b1) = f . b ) ) )
set G = f * F;
F is continuous
by A1, BORSUK_6:def 11;
hence
f * F is continuous
; for b1 being Element of the carrier of K523() holds
( (f * F) . (b1,0) = P1 . b1 & (f * F) . (b1,1) = Q1 . b1 & (f * F) . (0,b1) = f . a & (f * F) . (1,b1) = f . b )
let s be Point of I[01]; ( (f * F) . (s,0) = P1 . s & (f * F) . (s,1) = Q1 . s & (f * F) . (0,s) = f . a & (f * F) . (1,s) = f . b )
thus (f * F) . (s,0) =
f . (F . (s,j0))
by Lm1, BINOP_1:18
.=
f . (P . s)
by A1, BORSUK_6:def 11
.=
P1 . s
by A2, FUNCT_2:15
; ( (f * F) . (s,1) = Q1 . s & (f * F) . (0,s) = f . a & (f * F) . (1,s) = f . b )
thus (f * F) . (s,1) =
f . (F . (s,j1))
by Lm1, BINOP_1:18
.=
f . (Q . s)
by A1, BORSUK_6:def 11
.=
Q1 . s
by A3, FUNCT_2:15
; ( (f * F) . (0,s) = f . a & (f * F) . (1,s) = f . b )
thus (f * F) . (0,s) =
f . (F . (j0,s))
by Lm1, BINOP_1:18
.=
f . a
by A1, BORSUK_6:def 11
; (f * F) . (1,s) = f . b
thus (f * F) . (1,s) =
f . (F . (j1,s))
by Lm1, BINOP_1:18
.=
f . b
by A1, BORSUK_6:def 11
; verum