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[01] holds (P1 + Q1) . x = (f * (P + Q)) . x

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[01] holds (P1 + Q1) . x = (f * (P + Q)) . x

proof

hence
P1 + Q1 = f * (P + Q)
; :: thesis: verum
let x be Point of I[01]; :: thesis: (P1 + Q1) . x = (f * (P + Q)) . x

A4: ( f . a,f . b are_connected & f . b,f . c are_connected ) by A1, Th23;

end;A4: ( f . a,f . b are_connected & f . b,f . c are_connected ) by A1, Th23;

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

end;

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

then A6:
2 * x is Point of I[01]
by BORSUK_6:3;

thus (P1 + Q1) . x = P1 . (2 * x) by A4, A5, BORSUK_2:def 5

.= f . (P . (2 * x)) by A2, A6, FUNCT_2:15

.= f . ((P + Q) . x) by A1, A5, BORSUK_2:def 5

.= (f * (P + Q)) . x by FUNCT_2:15 ; :: thesis: verum

end;thus (P1 + Q1) . x = P1 . (2 * x) by A4, A5, BORSUK_2:def 5

.= f . (P . (2 * x)) by A2, A6, FUNCT_2:15

.= f . ((P + Q) . x) by A1, A5, BORSUK_2:def 5

.= (f * (P + Q)) . x by FUNCT_2:15 ; :: thesis: verum

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

then A8:
(2 * x) - 1 is Point of I[01]
by BORSUK_6:4;

thus (P1 + Q1) . x = Q1 . ((2 * x) - 1) by A4, A7, BORSUK_2:def 5

.= f . (Q . ((2 * x) - 1)) by A3, A8, FUNCT_2:15

.= f . ((P + Q) . x) by A1, A7, BORSUK_2:def 5

.= (f * (P + Q)) . x by FUNCT_2:15 ; :: thesis: verum

end;thus (P1 + Q1) . x = Q1 . ((2 * x) - 1) by A4, A7, BORSUK_2:def 5

.= f . (Q . ((2 * x) - 1)) by A3, A8, FUNCT_2:15

.= f . ((P + Q) . x) by A1, A7, BORSUK_2:def 5

.= (f * (P + Q)) . x by FUNCT_2:15 ; :: thesis: verum