let T be non empty TopSpace-like unital BinContinuous TopGrStr ; :: thesis: for t being unital Point of T

for f, g being Loop of t

for c being constant Loop of t holds f + g = LoopMlt ((f + c),(c + g))

let t be unital Point of T; :: thesis: for f, g being Loop of t

for c being constant Loop of t holds f + g = LoopMlt ((f + c),(c + g))

let f, g be Loop of t; :: thesis: for c being constant Loop of t holds f + g = LoopMlt ((f + c),(c + g))

let c be constant Loop of t; :: thesis: f + g = LoopMlt ((f + c),(c + g))

let x be Point of I[01]; :: according to FUNCT_2:def 8 :: thesis: (f + g) . x = (LoopMlt ((f + c),(c + g))) . x

A1: c = I[01] --> t by BORSUK_2:5;

for f, g being Loop of t

for c being constant Loop of t holds f + g = LoopMlt ((f + c),(c + g))

let t be unital Point of T; :: thesis: for f, g being Loop of t

for c being constant Loop of t holds f + g = LoopMlt ((f + c),(c + g))

let f, g be Loop of t; :: thesis: for c being constant Loop of t holds f + g = LoopMlt ((f + c),(c + g))

let c be constant Loop of t; :: thesis: f + g = LoopMlt ((f + c),(c + g))

let x be Point of I[01]; :: according to FUNCT_2:def 8 :: thesis: (f + g) . x = (LoopMlt ((f + c),(c + g))) . x

A1: c = I[01] --> t by BORSUK_2:5;

now :: thesis: (f + g) . x = ((f + c) . x) * ((c + g) . x)end;

hence
(f + g) . x = (LoopMlt ((f + c),(c + g))) . x
by Def2; :: thesis: verumper cases
( x <= 1 / 2 or x >= 1 / 2 )
;

end;

suppose A2:
x <= 1 / 2
; :: thesis: (f + g) . x = ((f + c) . x) * ((c + g) . x)

then reconsider z = 2 * x as Point of I[01] by BORSUK_6:3;

A3: (f + c) . x = f . z by A2, BORSUK_2:def 5;

(c + g) . x = c . z by A2, BORSUK_2:def 5

.= t by A1 ;

hence (f + g) . x = ((f + c) . x) * ((c + g) . x) by A2, A3, BORSUK_2:def 5; :: thesis: verum

end;A3: (f + c) . x = f . z by A2, BORSUK_2:def 5;

(c + g) . x = c . z by A2, BORSUK_2:def 5

.= t by A1 ;

hence (f + g) . x = ((f + c) . x) * ((c + g) . x) by A2, A3, BORSUK_2:def 5; :: thesis: verum

suppose A4:
x >= 1 / 2
; :: thesis: (f + g) . x = ((f + c) . x) * ((c + g) . x)

then reconsider z = (2 * x) - 1 as Point of I[01] by BORSUK_6:4;

A5: (f + c) . x = c . z by A4, BORSUK_2:def 5

.= t by A1 ;

(c + g) . x = g . z by A4, BORSUK_2:def 5;

hence (f + g) . x = ((f + c) . x) * ((c + g) . x) by A5, A4, BORSUK_2:def 5; :: thesis: verum

end;A5: (f + c) . x = c . z by A4, BORSUK_2:def 5

.= t by A1 ;

(c + g) . x = g . z by A4, BORSUK_2:def 5;

hence (f + g) . x = ((f + c) . x) * ((c + g) . x) by A5, A4, BORSUK_2:def 5; :: thesis: verum