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 and
A2: b,c are_connected and
A3: P1 = f * P and
A4: Q1 = f * Q ; :: thesis: P1 + Q1 = f * (P + Q)
for x being Point of I[01] holds (P1 + Q1) . x = (f * (P + Q)) . x

proof

let x be Point of I[01] ; :: thesis: (P1 + Q1) . x = (f * (P + Q)) . x
A5: f . a,f . b are_connected by A1, Th24;
A6: f . b,f . c are_connected by A2, Th24;

per cases ( x <= 1 / 2 or x >= 1 / 2 ) ;

suppose A7: x <= 1 / 2 ; :: thesis: (P1 + Q1) . x = (f * (P + Q)) . x

then A8: 2 * x is Point of I[01] by BORSUK_6:6;
thus (P1 + Q1) . x = P1 . (2 * x) by A5, A6, A7, BORSUK_2:def 5
.= f . (P . (2 * x)) by A3, A8, FUNCT_2:21
.= f . ((P + Q) . x) by A1, A2, A7, BORSUK_2:def 5
.= (f * (P + Q)) . x by FUNCT_2:21 ; :: thesis: verum

end;

suppose A9: x >= 1 / 2 ; :: thesis: (P1 + Q1) . x = (f * (P + Q)) . x

then A10: (2 * x) - 1 is Point of I[01] by BORSUK_6:7;
thus (P1 + Q1) . x = Q1 . ((2 * x) - 1) by A5, A6, A9, BORSUK_2:def 5
.= f . (Q . ((2 * x) - 1)) by A4, A10, FUNCT_2:21
.= f . ((P + Q) . x) by A1, A2, A9, BORSUK_2:def 5
.= (f * (P + Q)) . x by FUNCT_2:21 ; :: thesis: verum

end;

end;

end;

hence P1 + Q1 = f * (P + Q) by FUNCT_2:113; :: thesis: verum