let S, T be non empty TopSpace; for f being continuous Function of S,T
for a, b, c being Point of S
for P being Path of a,b
for Q being Path of b,c
for P1 being Path of f . a,f . b
for Q1 being Path of f . b,f . c st a,b are_connected & b,c are_connected & P1 = f * P & Q1 = f * Q holds
P1 + Q1 = f * (P + Q)
let f be continuous Function of S,T; for a, b, c being Point of S
for P being Path of a,b
for Q being Path of b,c
for P1 being Path of f . a,f . b
for Q1 being Path of f . b,f . c st a,b are_connected & b,c are_connected & P1 = f * P & Q1 = f * Q holds
P1 + Q1 = f * (P + Q)
let a, b, c be Point of S; for P being Path of a,b
for Q being Path of b,c
for P1 being Path of f . a,f . b
for Q1 being Path of f . b,f . c st a,b are_connected & b,c are_connected & P1 = f * P & Q1 = f * Q holds
P1 + Q1 = f * (P + Q)
let P be Path of a,b; for Q being Path of b,c
for P1 being Path of f . a,f . b
for Q1 being Path of f . b,f . c st a,b are_connected & b,c are_connected & P1 = f * P & Q1 = f * Q holds
P1 + Q1 = f * (P + Q)
let Q be Path of b,c; for P1 being Path of f . a,f . b
for Q1 being Path of f . b,f . c st a,b are_connected & b,c are_connected & P1 = f * P & Q1 = f * Q holds
P1 + Q1 = f * (P + Q)
let P1 be Path of f . a,f . b; for Q1 being Path of f . b,f . c st a,b are_connected & b,c are_connected & P1 = f * P & Q1 = f * Q holds
P1 + Q1 = f * (P + Q)
let Q1 be Path of f . b,f . c; ( a,b are_connected & b,c are_connected & P1 = f * P & Q1 = f * Q implies P1 + Q1 = f * (P + Q) )
assume that
A1:
( a,b are_connected & b,c are_connected )
and
A2:
P1 = f * P
and
A3:
Q1 = f * Q
; P1 + Q1 = f * (P + Q)
for x being Point of I[01] holds (P1 + Q1) . x = (f * (P + Q)) . x
hence
P1 + Q1 = f * (P + Q)
; verum