:: Commutativeness of Fundamental Groups of Topological Groups
::  by Artur Korni{\l}owicz
::
:: Received May 19, 2013
:: Copyright (c) 2013-2019 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, GROUP_1, RELAT_1, FUNCT_1, SUBSET_1, BORSUK_1, PRE_TOPC,
      CARD_1, XBOOLE_0, ARYTM_3, RCOMP_1, TARSKI, ORDINAL2, ZFMISC_1, BORSUK_2,
      ALGSTR_1, EQREL_1, WAYBEL20, ALGSTR_0, BINOP_1, BORSUK_6, TOPALG_1,
      TOPGRP_1, CONNSP_2, XXREAL_0, FUNCOP_1, STRUCT_0, ARYTM_1, VALUED_1,
      TOPMETR, SETFAM_1, TOPS_1, XXREAL_1, REALSET1, TOPALG_7, REAL_1, MCART_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, EQREL_1, FUNCT_1, RELSET_1,
      PARTFUN1, FUNCT_2, BINOP_1, REALSET1, FUNCT_3, NUMBERS, XCMPLX_0,
      XXREAL_0, XREAL_0, RCOMP_1, FUNCOP_1, STRUCT_0, ALGSTR_0, PRE_TOPC,
      TOPS_1, CONNSP_2, GROUP_1, GROUP_2, BORSUK_1, BORSUK_2, BORSUK_6,
      TOPMETR, TOPALG_1, TOPREALB, TOPGRP_1;
 constructors TOPS_1, REALSET2, GROUP_6, BORSUK_6, MONOID_0, TOPALG_1,
      TOPGRP_1, COMPTS_1, FUNCOP_1, TOPREALB;
 registrations XBOOLE_0, RELSET_1, FUNCT_2, XXREAL_0, XREAL_0, MEMBERED,
      STRUCT_0, TOPS_1, BORSUK_1, BORSUK_2, MONOID_0, PRE_TOPC, TOPALG_1,
      FUNCOP_1, TOPGRP_1, TOPMETR, TOPALG_3, ORDINAL1;
 requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
 definitions TARSKI, FUNCT_2, GROUP_1, BORSUK_1, BORSUK_2, BORSUK_6;
 equalities BINOP_1, REALSET1, STRUCT_0, GROUP_2, BORSUK_1, TOPALG_1, TOPREALB;
 expansions TARSKI, BORSUK_2;
 theorems TOPALG_1, GROUP_1, BORSUK_1, BORSUK_2, TOPGRP_1, XREAL_1, TARSKI,
      CONNSP_2, FUNCT_2, XBOOLE_0, FUNCOP_1, BORSUK_6, ZFMISC_1, PRE_TOPC,
      TOPS_1, TOPMETR, TOPREALA, REALSET1, FUNCT_1, TSEP_1, BORSUK_3, BINOP_1,
      JGRAPH_2, YELLOW12, FUNCT_3;
 schemes FUNCT_2, BINOP_1;

begin

set I = I[01];
set II = [:I,I:];
set R = R^1;
set RR = [:R,R:];
set A = R^1([.0,1.]);
set cR = the carrier of R;
Lm1: the carrier of RR = [:cR,cR:] by BORSUK_1:def 2;

definition
  let A,B be non empty TopSpace, C be set, f be Function of [:A,B:],C;
  let a be Element of A;
  let b be Element of B;
  redefine func f.(a,b) -> Element of C;
  coherence
  proof
    f. [a,b] is Element of C;
    hence thesis;
  end;
end;

definition
  let G be multMagma, g be Element of G;
  attr g is unital means :Def1:
  g = 1_G;
end;

registration
  let G be multMagma;
  cluster 1_G -> unital;
  coherence;
end;

registration
  let G be unital multMagma;
  cluster unital for Element of G;
  existence
  proof
    take 1_G;
    thus 1_G = 1_G;
  end;
end;

registration
  let G be unital multMagma, g be Element of G, h be unital Element of G;
  reduce g * h to g;
  reducibility
  proof
    h = 1_G by Def1;
    hence thesis by GROUP_1:def 4;
  end;
  reduce h * g to g;
  reducibility
  proof
    h = 1_G by Def1;
    hence thesis by GROUP_1:def 4;
  end;
end;

registration
  let G be Group;
  reduce (1_G)" to 1_G;
  reducibility by GROUP_1:8;
end;

scheme TopFuncEx
 { S,T() -> non empty TopSpace, X() -> non empty set,
   F(Point of S(),Point of T()) -> Element of X() } :
  ex f being Function of [:S(),T():],X() st
   for s being Point of S(), t being Point of T() holds f.(s,t) = F(s,t);
  consider f being Function of [:the carrier of S(),the carrier of T():],X()
  such that
A1: for x being Point of S(), y being Point of T() holds f.(x,y) = F(x,y)
  from BINOP_1:sch 4;
  [:the carrier of S(),the carrier of T():] = the carrier of [:S(),T():]
  by BORSUK_1:def 2;
  then reconsider f as Function of [:S(),T():],X();
  take f;
  thus thesis by A1;
end;

scheme TopFuncEq
 { S,T() -> non empty TopSpace, X() -> non empty set,
   F(Point of S(),Point of T()) -> Element of X() } :
 for f,g being Function of [:S(),T():],X() st
  (for s being Point of S(), t being Point of T() holds f.(s,t) = F(s,t)) &
  (for s being Point of S(), t being Point of T() holds g.(s,t) = F(s,t))
  holds f = g;
  let f,g be Function of [:S(),T():],X() such that
A1: for a being Point of S(), b being Point of T() holds f.(a,b) = F(a,b) and
A2: for a being Point of S(), b being Point of T() holds g.(a,b) = F(a,b);
  let x be Point of [:S(),T():];
  consider a being Point of S(), b being Point of T() such that
A3: x = [a,b] by BORSUK_1:10;
  thus f.x = f.(a,b) by A3
  .= F(a,b) by A1
  .= g.(a,b) by A2
  .= g.x by A3;
end;

definition
  let X be non empty set;
  let T be non empty multMagma;
  let f,g be Function of X,T;
  deffunc F(Element of X) = f.$1 * g.$1;
  func f(#)g -> Function of X,T means :Def2:
  for x being Element of X holds it.x = f.x * g.x;
  existence
  proof
    thus ex f being Function of X,T st
    for x being Element of X holds f.x = F(x) from FUNCT_2:sch 4;
  end;
  uniqueness
  proof
    let F,G be Function of X,T such that
A1: for x being Element of X holds F.x = F(x) and
A2: for x being Element of X holds G.x = F(x);
    let x be Element of X;
    thus F.x = F(x) by A1
    .= G.x by A2;
  end;
end;

theorem
  for X being non empty set, T being associative non empty multMagma
  for f,g,h being Function of X,T holds f(#)g(#)h = f(#)(g(#)h)
  proof
    let X be non empty set;
    let T be associative non empty multMagma;
    let f,g,h be Function of X,T;
    let x be Element of X;
    thus (f(#)g(#)h).x = (f(#)g).x*h.x by Def2
    .= f.x*g.x*h.x by Def2
    .= f.x*(g.x*h.x) by GROUP_1:def 3
    .= f.x*(g(#)h).x by Def2
    .= (f(#)(g(#)h)).x by Def2;
  end;

definition
 let X be non empty set, T be commutative non empty multMagma;
 let f,g be Function of X,T;
  redefine func f(#)g;
 commutativity
  proof let f,g be Function of X,T;
    let x be Element of X;
    thus (f(#)g).x = f.x*g.x by Def2
    .= (g(#)f).x by Def2;
  end;
end;

definition
  let T be non empty TopGrStr;
  let t be Point of T;
  let f,g be Loop of t;
  func LoopMlt(f,g) -> Function of I[01],T equals
  f(#)g;
  coherence;
end;

reserve T for BinContinuous unital TopSpace-like non empty TopGrStr,
  x,y for Point of I[01],
  s,t for unital Point of T,
  f,g for Loop of t,
  c for constant Loop of t;

definition
  let T,t,f,g;
  redefine func LoopMlt(f,g) -> Loop of t;
  coherence
  proof
    set F = LoopMlt(f,g);
    thus
A1: t,t are_connected;
    thus F is continuous
    proof
      let a be Point of I, G be a_neighborhood of F.a;
      F.a = f.a * g.a by Def2;
      then consider A being open a_neighborhood of f.a,
                    B being open a_neighborhood of g.a such that
A2:   A * B c= G by TOPGRP_1:37;
      consider Ha being a_neighborhood of a such that
A3:   f.:Ha c= A by BORSUK_1:def 1;
      consider Hb being a_neighborhood of a such that
A4:   g.:Hb c= B by BORSUK_1:def 1;
      reconsider H = Ha /\ Hb as a_neighborhood of a by CONNSP_2:2;
      take H;
      F.:H c= A * B
      proof
        let y be object;
        assume y in F.:H;
        then consider c being Element of I such that
A5:     c in H and
A6:     F.c = y by FUNCT_2:65;
A7:     F.c = f.c * g.c by Def2;
        c in Ha & c in Hb by A5,XBOOLE_0:def 4;
        then f.c in f.:Ha & g.c in g.:Hb by FUNCT_2:35;
        hence thesis by A3,A4,A6,A7;
      end;
      hence F.:H c= G by A2;
    end;
A8: t = 1_T by Def1;
A9: 1_T * 1_T = 1_T;
    f.0[01] = t & g.0[01] = t & f.1[01] = t & g.1[01] = t by A1,BORSUK_2:def 2;
    hence thesis by A8,A9,Def2;
  end;
end;

registration
  let T be UnContinuous TopGroup;
  cluster inverse_op(T) -> continuous;
  coherence;
end;

definition
  let T be TopGroup, t be Point of T, f be Loop of t;
  func inverse_loop(f) -> Function of I[01],T equals
  inverse_op(T) * f;
  coherence;
end;

theorem Th2:
  for T being TopGroup, t being Point of T, f being Loop of t holds
  inverse_loop(f).x = (f.x)"
  proof
    let T be TopGroup;
    let t be Point of T;
    let f be Loop of t;
    thus inverse_loop(f).x = inverse_op(T).(f.x) by FUNCT_2:15
    .= (f.x)" by GROUP_1:def 6;
  end;

theorem Th3:
  for T being TopGroup, t being Point of T, f being Loop of t holds
  inverse_loop(f).x * f.x = 1_T
  proof
    let T be TopGroup, t be Point of T, f be Loop of t;
    inverse_loop(f).x = (f.x)" by Th2;
    hence thesis by GROUP_1:def 5;
  end;

theorem
  for T being TopGroup, t being Point of T, f being Loop of t holds
  f.x * inverse_loop(f).x = 1_T
  proof
    let T be TopGroup, t be Point of T, f be Loop of t;
    inverse_loop(f).x = (f.x)" by Th2;
    hence thesis by GROUP_1:def 5;
  end;

definition
  let T be UnContinuous TopGroup,t be unital Point of T,f be Loop of t;
  redefine func inverse_loop(f) -> Loop of t;
  coherence
  proof
    thus
A1: t,t are_connected;
    thus inverse_loop(f) is continuous;
A2: t = 1_T by Def1;
A3: (1_T)" = 1_T;
    f.0[01] = t & f.1[01] = t by A1,BORSUK_2:def 2;
    hence thesis by A2,A3,Th2;
  end;
end;

definition
  let s,t be Point of I[01];
  redefine func s*t -> Point of I[01];
  coherence
  proof
    0 <= s & 0 <= t & s <= 1 & t <= 1 by BORSUK_1:43;
    hence thesis by BORSUK_1:43,XREAL_1:160;
  end;
end;

definition
  func R^1-TIMES -> Function of [:R^1,R^1:],R^1 means :Def5:
  for x,y being Point of R^1 holds it.(x,y) = x*y;
  existence
  proof
    deffunc F(Point of R,Point of R) = R^1($1*$2);
    consider f being Function of RR,R such that
A1: for s,t being Point of R holds f.(s,t) = F(s,t) from TopFuncEx;
    take f;
    let x,y be Point of R;
    f.(x,y) = F(x,y) by A1;
    hence thesis;
  end;
  uniqueness
  proof
    let f,g be Function of RR,R such that
A2: for x,y being Point of R holds f.(x,y) = x*y and
A3: for x,y being Point of R holds g.(x,y) = x*y;
    now
      let x,y be Point of R;
      thus f.(x,y) = x*y by A2
      .= g.(x,y) by A3;
    end;
    hence thesis by Lm1,BINOP_1:2;
  end;
end;

registration
  cluster R^1-TIMES -> continuous;
  coherence
  proof
    reconsider f1 = pr1(cR,cR) as continuous Function of RR,R by YELLOW12:39;
    reconsider f2 = pr2(cR,cR) as continuous Function of RR,R by YELLOW12:40;
    consider g being Function of RR,R such that
A1: for p being Point of RR, r1,r2 being Real st f1.p = r1 & f2.p = r2 holds
    g.p = r1*r2 and
A2: g is continuous by JGRAPH_2:25;
    now
      let a,b be Point of R;
A3:   f1.(a,b) = a & f2.(a,b) = b by FUNCT_3:def 4,def 5;
      thus R^1-TIMES.(a,b) = a*b by Def5
      .= g. [a,b] by A1,A3
      .= g.(a,b);
    end;
    hence thesis by A2,Lm1,BINOP_1:2;
  end;
end;

theorem Th5:
  [:R^1,R^1:] | [:R^1([.0,1.]),R^1([.0,1.]):] = [:I[01],I[01]:]
  proof
A1: II is SubSpace of RR by BORSUK_3:21;
    the carrier of II = [:A,A:] by BORSUK_1:def 2,40;
    hence thesis by A1,TSEP_1:5,PRE_TOPC:8;
  end;

definition
  func I[01]-TIMES -> Function of [:I[01],I[01]:],I[01] equals
  R^1-TIMES || R^1([.0,1.]);
  coherence
  proof
    reconsider f = R^1-TIMES as BinOp of cR by Lm1;
    for x being set holds x in [:A,A:] implies f.x in A
    proof
      let x be set;
      assume x in [:A,A:];
      then consider a,b being object such that
A1:   a in A & b in A and
A2:   x = [a,b] by ZFMISC_1:def 2;
      reconsider a,b as Point of I by A1,BORSUK_1:40;
      reconsider a1 = a, b1 = b as Point of R by A1;
      f.(a1,b1) = a*b by Def5;
      hence f.x in A by A2,BORSUK_1:40;
    end;
    then reconsider A as Preserv of f by REALSET1:def 1;
A3: the carrier of II = [:the carrier of I,the carrier of I:]
    by BORSUK_1:def 2;
    f || A is BinOp of A;
    hence thesis by A3,BORSUK_1:40;
  end;
end;

theorem Th6:
  I[01]-TIMES.(x,y) = x*y
  proof
    x is Point of R & y is Point of R by PRE_TOPC:25;
    hence x*y = R^1-TIMES.(x,y) by Def5
    .= I[01]-TIMES.(x,y) by FUNCT_1:49,ZFMISC_1:87,BORSUK_1:40;
  end;

registration
  cluster I[01]-TIMES -> continuous;
  coherence
  proof
    reconsider f = I[01]-TIMES as Function of II,R by TOPREALA:7;
    f is continuous by Th5,TOPMETR:7;
    hence thesis by PRE_TOPC:27;
  end;
end;

theorem Th7:
  for a,b being Point of I[01] holds
  for N being a_neighborhood of a*b
  ex N1 being a_neighborhood of a, N2 being a_neighborhood of b st
  for x,y being Point of I[01] st x in N1 & y in N2 holds x*y in N
  proof
    let a,b be Point of I;
    let N be a_neighborhood of a*b;
    set g = I[01]-TIMES;
    g.(a,b) = a*b by Th6;
    then consider H being a_neighborhood of [a,b] such that
A1: g.:H c= N by BORSUK_1:def 1;
    consider F being Subset-Family of [:I,I:] such that
A2: Int H = union F and
A3: for e being set st e in F ex X1, Y1 being Subset of I st e = [:X1,Y1:] &
    X1 is open & Y1 is open by BORSUK_1:5;
    [a,b] in Int H by CONNSP_2:def 1;
    then consider M being set such that
A4: [a,b] in M and
A5: M in F by A2,TARSKI:def 4;
    consider A, B being Subset of I such that
A6: M = [:A,B:] and
A7: A is open and
A8: B is open by A3,A5;
    a in A by A4,A6,ZFMISC_1:87;
    then
A9: a in Int A by A7,TOPS_1:23;
    b in B by A4,A6,ZFMISC_1:87;
    then b in Int B by A8,TOPS_1:23;
    then reconsider B as open a_neighborhood of b by A8,CONNSP_2:def 1;
    reconsider A as open a_neighborhood of a by A7,A9,CONNSP_2:def 1;
    take A,B;
    let x,y be Point of I such that
A10: x in A & y in B;
A11: Int H c= H by TOPS_1:16;
A12: g.(x,y) = x*y by Th6;
    [x,y] in M by A6,A10,ZFMISC_1:87;
    then [x,y] in Int H by A2,A5,TARSKI:def 4;
    then g.(x,y) in g.:H by A11,FUNCT_2:35;
    hence thesis by A1,A12;
  end;

definition
  let T be non empty multMagma;
  let F,G be Function of [:I[01],I[01]:],T;
  deffunc F(Point of I,Point of I) = F.($1,$2) * G.($1,$2);
  func HomotopyMlt(F,G) -> Function of [:I[01],I[01]:],T means :Def7:
  for a,b being Point of I[01] holds it.(a,b) = F.(a,b) * G.(a,b);
  existence
  proof
    thus ex f being Function of II,T st
    for a,b being Point of I holds f.(a,b) = F(a,b) from TopFuncEx;
  end;
  uniqueness
  proof
    thus for f,g being Function of II,T st
    (for a,b being Point of I holds f.(a,b) = F(a,b)) &
    (for a,b being Point of I holds g.(a,b) = F(a,b)) holds f = g
    from TopFuncEq;
  end;
end;

Lm2: now
  let T,t,x;
  let f1,f2,g1,g2 be Loop of t,
      F be Homotopy of f1,f2, G be Homotopy of g1,g2;
  assume
A1: f1,f2 are_homotopic & g1,g2 are_homotopic;
  then
A2: F.(x,0[01]) = f1.x & G.(x,0[01]) = g1.x by BORSUK_6:def 11;
  thus HomotopyMlt(F,G).(x,0) = F.(x,0[01]) * G.(x,0[01]) by Def7
  .= LoopMlt(f1,g1).x by A2,Def2;
A3: F.(x,1[01]) = f2.x & G.(x,1[01]) = g2.x by A1,BORSUK_6:def 11;
  thus HomotopyMlt(F,G).(x,1) = F.(x,1[01]) * G.(x,1[01]) by Def7
  .= LoopMlt(f2,g2).x by A3,Def2;
  F.(0[01],x) = t & G.(0[01],x) = t by A1,BORSUK_6:def 11;
  hence HomotopyMlt(F,G).(0,x) = t * t by Def7
  .= t;
  F.(1[01],x) = t & G.(1[01],x) = t by A1,BORSUK_6:def 11;
  hence HomotopyMlt(F,G).(1,x) = t * t by Def7
  .= t;
end;

theorem Th8:
  for F,G being Function of [:I[01],I[01]:],T
  for M,N being Subset of [:I[01],I[01]:] holds
  HomotopyMlt(F,G).:(M/\N) c= F.:M * G.:N
  proof
    let F,G be Function of II,T;
    let M,N be Subset of II;
    let y be object;
    assume y in HomotopyMlt(F,G).:(M/\N);
    then consider x being Point of II such that
A1: x in M /\ N and
A2: HomotopyMlt(F,G).x = y by FUNCT_2:65;
    consider a,b being Point of I such that
A3: x = [a,b] by BORSUK_1:10;
A4: HomotopyMlt(F,G).(a,b) = F.(a,b) * G.(a,b) by Def7;
    [a,b] in M & [a,b] in N by A1,A3,XBOOLE_0:def 4;
    then F.(a,b) in F.:M & G.(a,b) in G.:N by FUNCT_2:35;
    hence thesis by A2,A3,A4;
  end;

registration
  let T;
  let F,G be continuous Function of [:I[01],I[01]:],T;
  cluster HomotopyMlt(F,G) -> continuous;
  coherence
  proof
    let W be Point of II,
        N be a_neighborhood of HomotopyMlt(F,G).W;
    consider a,b being Point of I such that
A1: W = [a,b] by BORSUK_1:10;
    HomotopyMlt(F,G).(a,b) = F.(a,b) * G.(a,b) by Def7;
    then consider A being open a_neighborhood of F.(a,b),
                  B being open a_neighborhood of G.(a,b) such that
A2: A * B c= N by A1,TOPGRP_1:37;
    consider NF being a_neighborhood of [a,b] such that
A3: F.:NF c= A by BORSUK_1:def 1;
    consider NG being a_neighborhood of [a,b] such that
A4: G.:NG c= B by BORSUK_1:def 1;
    reconsider H = NF /\ NG as a_neighborhood of W by A1,CONNSP_2:2;
    take H;
A5: HomotopyMlt(F,G).:(NF/\NG) c= F.:NF * G.:NG by Th8;
    F.:NF * G.:NG c= A * B by A3,A4,TOPGRP_1:4;
    hence thesis by A5,A2;
  end;
end;

theorem Th9:
  for f1,f2,g1,g2 being Loop of t
  st f1,f2 are_homotopic & g1,g2 are_homotopic holds
  LoopMlt(f1,g1),LoopMlt(f2,g2) are_homotopic
  proof
    let f1,f2,g1,g2 be Loop of t;
    assume
A1: f1,f2 are_homotopic;
    then consider F being Function of II,T such that
A2: F is continuous &
    for x being Point of I holds F.(x,0) = f1.x & F.(x,1) = f2.x &
    F.(0,x) = t & F.(1,x) = t;
    assume
A3: g1,g2 are_homotopic;
    then consider G being Function of II,T such that
A4: G is continuous &
    for x being Point of I holds G.(x,0) = g1.x & G.(x,1) = g2.x &
    G.(0,x) = t & G.(1,x) = t;
    take HomotopyMlt(F,G);
    F is Homotopy of f1,f2 & G is Homotopy of g1,g2
    by A2,A4,A1,A3,BORSUK_6:def 11;
    hence thesis by A1,A2,A3,A4,Lm2;
  end;

theorem
  for f1,f2,g1,g2 being Loop of t,
      F being Homotopy of f1,f2, G being Homotopy of g1,g2
  st f1,f2 are_homotopic & g1,g2 are_homotopic holds
  HomotopyMlt(F,G) is Homotopy of LoopMlt(f1,g1),LoopMlt(f2,g2)
  proof
    let f1,f2,g1,g2 be Loop of t,
        F be Homotopy of f1,f2, G be Homotopy of g1,g2 such that
A1: f1,f2 are_homotopic & g1,g2 are_homotopic;
    thus LoopMlt(f1,g1),LoopMlt(f2,g2) are_homotopic by A1,Th9;
    F is continuous & G is continuous by A1,BORSUK_6:def 11;
    hence HomotopyMlt(F,G) is continuous;
    thus thesis by A1,Lm2;
  end;

theorem Th11:
  f+g = LoopMlt(f+c,c+g)
  proof
    let x;
A1: c = I --> t by BORSUK_2:5;
    now per cases;
      suppose
A2:     x <= 1/2;
        then reconsider z = 2*x as Point of I 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;
      end;
      suppose
A4:     x >= 1/2;
        then reconsider z = 2*x-1 as Point of I 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;
      end;
    end;
    hence thesis by Def2;
  end;

theorem Th12:
  LoopMlt(f,g),LoopMlt(f+c,c+g) are_homotopic
  proof
    f,f+c are_homotopic & c+g,g are_homotopic by BORSUK_6:80,82;
    hence thesis by Th9;
  end;

definition
  let T be TopGroup,t be Point of T,f,g be Loop of t;
  deffunc F(Point of I,Point of I) =
  inverse_loop(f).($1*$2) * f.$1 * g.$1 * f.($1*$2);
  func HopfHomotopy(f,g) -> Function of [:I[01],I[01]:],T means :Def8:
  for a,b being Point of I[01] holds
  it.(a,b) = inverse_loop(f).(a*b) * f.a * g.a * f.(a*b);
  existence
  proof
    thus ex F being Function of II,T st
    for x,y being Point of I holds F.(x,y) = F(x,y) from TopFuncEx;
  end;
  uniqueness
  proof
    thus for f,g being Function of II,T st
    (for a,b being Point of I holds f.(a,b) = F(a,b)) &
    (for a,b being Point of I holds g.(a,b) = F(a,b)) holds f = g
    from TopFuncEq;
  end;
end;

registration
  let T be TopologicalGroup, t be Point of T, f,g be Loop of t;
  cluster HopfHomotopy(f,g) -> continuous;
  coherence
  proof
    set F = HopfHomotopy(f,g);
    set i = inverse_loop(f);
    let W be Point of II,
        G be a_neighborhood of F.W;
    consider a,b being Point of I such that
A1: W = [a,b] by BORSUK_1:10;
    F.(a,b) = i.(a*b) * f.a * g.a * f.(a*b) by Def8;
    then consider A1 being open a_neighborhood of i.(a*b) * f.a * g.a,
                  B1 being open a_neighborhood of f.(a*b) such that
A2: A1*B1 c= G by A1,TOPGRP_1:37;
    consider A2 being open a_neighborhood of i.(a*b) * f.a,
             B2 being open a_neighborhood of g.a such that
A3: A2*B2 c= A1 by TOPGRP_1:37;
    consider A3 being open a_neighborhood of i.(a*b),
             B3 being open a_neighborhood of f.a such that
A4: A3*B3 c= A2 by TOPGRP_1:37;
    i.(a*b) = inverse_op(T).(f.(a*b)) by FUNCT_2:15
    .= (f.(a*b))" by GROUP_1:def 6;
    then consider A4 being open a_neighborhood of f.(a*b) such that
A5: A4" c= A3 by TOPGRP_1:39;
    consider A5 being a_neighborhood of a*b such that
A6: f.:A5 c= A4 by BORSUK_1:def 1;
    consider NB1 being a_neighborhood of a*b such that
A7: f.:NB1 c= B1 by BORSUK_1:def 1;
    consider NB2 being a_neighborhood of a such that
A8: g.:NB2 c= B2 by BORSUK_1:def 1;
    consider NB3 being a_neighborhood of a such that
A9: f.:NB3 c= B3 by BORSUK_1:def 1;
    A5/\NB1 is a_neighborhood of a*b by CONNSP_2:2;
    then consider N1 being a_neighborhood of a,
                  N2 being a_neighborhood of b such that
A10: for x,y being Point of I st x in N1 & y in N2 holds x*y in A5/\NB1 by Th7;
    N1/\NB2 is a_neighborhood of a by CONNSP_2:2;
    then reconsider Na = N1/\NB2/\NB3 as a_neighborhood of a by CONNSP_2:2;
    reconsider H = [:Na,N2:] as a_neighborhood of W by A1;
    take H;
    let y be object;
    assume y in F.:H;
    then consider x being Element of II such that
A11: x in H and
A12: F.x = y by FUNCT_2:65;
    consider c,d being Point of I such that
A13: x = [c,d] by BORSUK_1:10;
A14: i.(c*d) = inverse_op(T).(f.(c*d)) by FUNCT_2:15
    .= (f.(c*d))" by GROUP_1:def 6;
A15: F.(c,d) = i.(c*d) * f.c * g.c * f.(c*d) by Def8;
A16: c in N1/\NB2/\NB3 by A11,A13,ZFMISC_1:87;
A17: c in N1/\NB2 by A16,XBOOLE_0:def 4;
    then
A18: c in N1 by XBOOLE_0:def 4;
    d in N2 by A11,A13,ZFMISC_1:87;
    then
A19: c*d in A5/\NB1 by A18,A10;
    then c*d in A5 by XBOOLE_0:def 4;
    then f.(c*d) in f.:A5 by FUNCT_2:35;
    then
A20: (f.(c*d))" in A4" by A6;
    c in NB3 by A16,XBOOLE_0:def 4;
    then f.c in f.:NB3 by FUNCT_2:35;
    then
A21: i.(c*d)*f.c in A3*B3 by A5,A9,A14,A20;
    c in NB2 by A17,XBOOLE_0:def 4;
    then g.c in g.:NB2 by FUNCT_2:35;
    then
A22: i.(c*d)*f.c*g.c in A2*B2 by A4,A8,A21;
    c*d in NB1 by A19,XBOOLE_0:def 4;
    then f.(c*d) in f.:NB1 by FUNCT_2:35;
    then i.(c*d)*f.c*g.c*f.(c*d) in A1*B1 by A3,A7,A22;
    hence thesis by A2,A12,A13,A15;
  end;
end;

reserve
  T for TopologicalGroup,
  t for unital Point of T,
  f,g for Loop of t;

Lm3: now
  let T,t,f,g,x;
  set F = HopfHomotopy(f,g);
  set i = inverse_loop(f);
A1: t = 1_T by Def1;
A2: t,t are_connected;
A3: f.0[01] = t by A2,BORSUK_2:def 2;
A4: f.1[01] = t by A2,BORSUK_2:def 2;
A5: g.0[01] = t by A2,BORSUK_2:def 2;
A6: i.0[01] = t by A2,BORSUK_2:def 2;
  thus F.(x,0) = i.(x*0[01]) * f.x * g.x * f.(x*0[01]) by Def8
  .= LoopMlt(f,g).x by A3,A6,Def2;
  thus F.(x,1) = i.(x*1[01]) * f.x * g.x * f.(x*1[01]) by Def8
  .= t * g.x * f.x by A1,Th3
  .= LoopMlt(g,f).x by Def2;
  thus F.(0,x) = i.(0[01]*x) * f.0[01] * g.0[01] * f.(0[01]*x) by Def8
  .= t by A3,A5,A2,BORSUK_2:def 2;
  thus F.(1,x) = i.(1[01]*x) * f.1[01] * g.1[01] * f.(1[01]*x) by Def8
  .= i.x * t * t * f.x by A4,A2,BORSUK_2:def 2
  .= t by A1,Th3;
end;

theorem Th13:
  LoopMlt(f,g),LoopMlt(g,f) are_homotopic
  proof
    take HopfHomotopy(f,g);
    thus thesis by Lm3;
  end;

definition
  let T,t,f,g;
  redefine func HopfHomotopy(f,g) -> Homotopy of LoopMlt(f,g),LoopMlt(g,f);
  coherence
  proof
    thus LoopMlt(f,g),LoopMlt(g,f) are_homotopic by Th13;
    thus thesis by Lm3;
  end;
end;

registration
  let T,t;
  cluster pi_1(T,t) -> commutative;
  coherence
  proof
    set c = the constant Loop of t;
    set E = EqRel(T,t);
    let x,y be Element of pi_1(T,t);
    consider f being Loop of t such that
A1: x = Class(E,f) by TOPALG_1:47;
    consider g being Loop of t such that
A2: y = Class(E,g) by TOPALG_1:47;
A3: x * y = Class(E,f+g) & y * x = Class(E,g+f) by A1,A2,TOPALG_1:61;
A4: f+g = LoopMlt(f+c,c+g) & g+f = LoopMlt(g+c,c+f) by Th11;
A5: LoopMlt(f,g),LoopMlt(f+c,c+g) are_homotopic by Th12;
A6: LoopMlt(g,f),LoopMlt(g+c,c+f) are_homotopic by Th12;
    LoopMlt(f,g),LoopMlt(g,f) are_homotopic by Th13;
    then LoopMlt(f,g), LoopMlt(g+c,c+f) are_homotopic by A6,BORSUK_6:79;
    then LoopMlt(f+c,c+g),LoopMlt(g+c,c+f) are_homotopic by A5,BORSUK_6:79;
    hence thesis by A3,A4,TOPALG_1:46;
  end;
end;