let T be non empty TopSpace; :: thesis: for a, b being Point of T
for P being Path of a,b
for Q being constant Path of a,a st a,b are_connected holds
RePar P,2RP = Q + P
let a, b be Point of T; :: thesis: for P being Path of a,b
for Q being constant Path of a,a st a,b are_connected holds
RePar P,2RP = Q + P
let P be Path of a,b; :: thesis: for Q being constant Path of a,a st a,b are_connected holds
RePar P,2RP = Q + P
let Q be constant Path of a,a; :: thesis: ( a,b are_connected implies RePar P,2RP = Q + P )
assume A1:
a,b are_connected
; :: thesis: RePar P,2RP = Q + P
A2:
a,a are_connected
;
set f = RePar P,2RP ;
set g = Q + P;
for p being Element of I[01] holds (RePar P,2RP ) . p = (Q + P) . p
proof
let p be
Element of
I[01] ;
:: thesis: (RePar P,2RP ) . p = (Q + P) . p
p in the
carrier of
I[01]
;
then A3:
p in dom 2RP
by FUNCT_2:def 1;
0 in the
carrier of
I[01]
by BORSUK_1:86;
then A4:
0 in dom Q
by FUNCT_2:def 1;
A5:
(RePar P,2RP ) . p =
(P * 2RP ) . p
by A1, Def6, Th56
.=
P . (2RP . p)
by A3, FUNCT_1:23
;
per cases
( p <= 1 / 2 or p > 1 / 2 )
;
suppose A6:
p <= 1
/ 2
;
:: thesis: (RePar P,2RP ) . p = (Q + P) . pthen
2
* p is
Point of
I[01]
by Th6;
then
2
* p in the
carrier of
I[01]
;
then A7:
2
* p in dom Q
by FUNCT_2:def 1;
(RePar P,2RP ) . p =
P . 0
by A5, A6, Def8
.=
a
by A1, BORSUK_2:def 2
.=
Q . 0
by A2, BORSUK_2:def 2
.=
Q . (2 * p)
by A4, A7, FUNCT_1:def 16
.=
(Q + P) . p
by A1, A6, BORSUK_2:def 5
;
hence
(RePar P,2RP ) . p = (Q + P) . p
;
:: thesis: verum end;
end;
hence
RePar P,2RP = Q + P
by FUNCT_2:113; :: thesis: verum