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
proof
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;
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[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;
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;
end;
end;
hence P1 + Q1 = f * (P + Q) ; :: thesis: verum