set R = the BinOp of {{}};
1TopSp {{}} is 1 -element ;
then reconsider T = TopaddGrStr(# {{}}, the BinOp of {{}},(bool {{}}) #) as 1 -element TopSpace-like strict TopaddGrStr by TEX_2:7;
take T ; :: thesis: ( T is strict & T is Abelian & T is UnContinuous & T is BinContinuous )
thus ( T is strict & T is Abelian ) ; :: thesis: ( T is UnContinuous & T is BinContinuous )
hereby :: according to GROUP_1A:def 46 :: thesis: T is BinContinuous
set f = add_inverse T;
thus add_inverse T is continuous :: thesis: verum
proof
let P1 be Subset of T; :: according to PRE_TOPC:def 6 :: thesis: ( not P1 is closed or (add_inverse T) " P1 is closed )
assume P1 is closed ; :: thesis: (add_inverse T) " P1 is closed
end;
end;
let f be Function of [:T,T:],T; :: according to GROUP_1A:def 47 :: thesis: ( f = the addF of T implies f is continuous )
assume f = the addF of T ; :: thesis: f is continuous
A1: the carrier of [:T,T:] = [:{{}},{{}}:] by BORSUK_1:def 2
.= {[{},{}]} by ZFMISC_1:29 ;
let P1 be Subset of T; :: according to PRE_TOPC:def 6 :: thesis: ( not P1 is closed or f " P1 is closed )
assume P1 is closed ; :: thesis: f " P1 is closed
per cases ( f " P1 = {} or f " P1 = {[{},{}]} ) by A1, ZFMISC_1:33;
suppose f " P1 = {} ; :: thesis: f " P1 is closed
hence f " P1 is closed ; :: thesis: verum
end;
suppose f " P1 = {[{},{}]} ; :: thesis: f " P1 is closed
then f " P1 = [#] [:T,T:] by A1;
hence f " P1 is closed ; :: thesis: verum
end;
end;