let S, T be non empty TopSpace; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: P1 + Q1 = f * (P + Q)
for x being Point of I holds (P1 + Q1) . x = (f * (P + Q)) . x
proof
let x be Point of I; :: thesis: (P1 + Q1) . x = (f * (P + Q)) . x
A4: ( f . a,f . b are_connected & f . b,f . c are_connected ) by ;
per cases ( x <= 1 / 2 or x >= 1 / 2 ) ;
suppose A5: x <= 1 / 2 ; :: thesis: (P1 + Q1) . x = (f * (P + Q)) . x
then A6: 2 * x is Point of I by BORSUK_6:3;
thus (P1 + Q1) . x = P1 . (2 * x) by
.= f . (P . (2 * x)) by
.= f . ((P + Q) . x) by
.= (f * (P + Q)) . x by FUNCT_2:15 ; :: thesis: verum
end;
suppose A7: x >= 1 / 2 ; :: thesis: (P1 + Q1) . x = (f * (P + Q)) . x
then A8: (2 * x) - 1 is Point of I by BORSUK_6:4;
thus (P1 + Q1) . x = Q1 . ((2 * x) - 1) by
.= f . (Q . ((2 * x) - 1)) by
.= f . ((P + Q) . x) by
.= (f * (P + Q)) . x by FUNCT_2:15 ; :: thesis: verum
end;
end;
end;
hence P1 + Q1 = f * (P + Q) ; :: thesis: verum