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;

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

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

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;

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;

end;

end;

hence (f + g) . x = (LoopMlt ((f + c),(c + g))) . x by Def2; :: thesis: verum