AFVECT0

:: Directed Geometrical Bundles and Their Analytical Representation
::  by Grzegorz Lewandowski, Krzysztof Pra\.zmowski and Bo\.zena Lewandowska
::
:: Received September 24, 1990
:: Copyright (c) 1990-2026 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 XBOOLE_0, ANALOAF, SUBSET_1, STRUCT_0, ZFMISC_1, TDGROUP, DIRAF,
      BINOP_1, FUNCT_1, ALGSTR_0, SUPINF_2, ARYTM_3, RLVECT_1, ARYTM_1,
      VECTSP_1, MCART_1, PBOOLE, RELAT_1, TARSKI, AFVECT0;
 notations TARSKI, ZFMISC_1, SUBSET_1, STRUCT_0, ALGSTR_0, ANALOAF, TDGROUP,
      FUNCT_1, FUNCT_2, XTUPLE_0, MCART_1, BINOP_1, RELAT_1, VECTSP_1,
      RLVECT_1;
 constructors BINOP_1, DOMAIN_1, TDGROUP, RELSET_1, XTUPLE_0;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, VECTSP_1, TDGROUP,
      RELAT_1, XTUPLE_0;
 requirements SUBSET, BOOLE;
 definitions RLVECT_1, ALGSTR_0;
 equalities STRUCT_0, BINOP_1, ALGSTR_0;
 expansions STRUCT_0;
 theorems DOMAIN_1, TDGROUP, FUNCT_1, FUNCT_2, MCART_1, RELAT_1, TARSKI,
      RLVECT_1, ANALOAF, XBOOLE_0, VECTSP_1, STRUCT_0;
 schemes BINOP_1, FUNCT_2;

begin

definition
  let IT be non empty AffinStruct;
  attr IT is WeakAffVect-like means
  :Def1:
  (for a,b,c being Element of IT st a
,b // c,c holds a=b) & (for a,b,c,d,p,q being Element of IT st a,b // p,q & c,d
// p,q holds a,b // c,d) & (for a,b,c being Element of IT ex d being Element of
IT st a,b // c,d) & (for a,b,c,a9,b9,c9 being Element of IT st a,b // a9,b9 & a
  ,c // a9,c9 holds b,c // b9,c9) & (for a,c being Element of IT ex b being
  Element of IT st a,b // b,c) & for a,b,c,d being Element of IT st a,b // c,d
  holds a,c // b,d;
end;

registration
  cluster strict WeakAffVect-like for non trivial AffinStruct;
  existence
  proof
    set AFV = the strict AffVect;
    reconsider AS = AFV as non empty AffinStruct;
A1: ( for a,b,c being Element of AS ex d being Element of AS st a,b // c,d
)& for a,b,c,a9,b9,c9 being Element of AS st a,b // a9,b9 & a,c // a9,c9 holds
    b,c // b9,c9 by TDGROUP:16;
A2: ( for a,c being Element of AS ex b being Element of AS st a,b // b,c)&
for a,b,c,d being Element of AS st a,b // c,d holds a,c // b,d by TDGROUP:16;
    ( for a,b,c being Element of AS st a,b // c,c holds a=b)& for a,b,c,d,
p,q being Element of AS st a,b // p,q & c,d // p,q holds a, b // c,d by
TDGROUP:16;
    then AS is WeakAffVect-like by A1,A2;
    hence thesis;
  end;
end;

definition
  mode WeakAffVect is WeakAffVect-like non trivial AffinStruct;
end;

registration
  cluster AffVect-like -> WeakAffVect-like for non empty AffinStruct;
  coherence
  by TDGROUP:def 5;
end;

reserve AFV for WeakAffVect;
reserve a,b,c,d,e,f,a9,b9,c9,d9,f9,p,q,r,o,x99 for Element of AFV;

::
::          Properties of Relation of Congruence of Vectors
::

theorem Th1:
  a,b // a,b
proof
  ex d st a,b // b,d by Def1;
  hence thesis by Def1;
end;

theorem
  a,a // a,a by Th1;

theorem Th3:
  a,b // c,d implies c,d // a,b
proof
  assume
A1: a,b // c,d;
  c,d // c,d by Th1;
  hence thesis by A1,Def1;
end;

theorem Th4:
  a,b // a,c implies b = c
proof
  assume a,b // a,c;
  then a,a // b,c by Def1;
  then b,c // a,a by Th3;
  hence thesis by Def1;
end;

theorem Th5:
  a,b // c,d & a,b // c,d9 implies d = d9
proof
  assume a,b // c,d & a,b // c,d9;
  then c,d // a,b & c,d9 // a,b by Th3;
  then c,d // c,d9 by Def1;
  hence thesis by Th4;
end;

theorem Th6:
  for a,b holds a,a // b,b
proof
  let a,b;
  consider p such that
A1: a,a // b,p by Def1;
  b,p // a,a by A1,Th3;
  hence thesis by A1,Def1;
end;

theorem Th7:
  a,b // c,d implies b,a // d,c
proof
  assume
A1: a,b // c,d;
  a,a // c,c by Th6;
  hence thesis by A1,Def1;
end;

theorem
  a,b // c,d & a,c // b9,d implies b = b9
proof
  assume that
A1: a,b // c,d and
A2: a,c // b9,d;
  a,c // b,d by A1,Def1;
  then b,d // a,c by Th3;
  then
A3: d,b // c,a by Th7;
  b9,d // a,c by A2,Th3;
  then d,b9 // c,a by Th7;
  then d,b // d,b9 by A3,Def1;
  hence thesis by Th4;
end;

theorem
  b,c // b9,c9 & a,d // b,c & a,d9 // b9,c9 implies d = d9
proof
  assume that
A1: b,c // b9,c9 and
A2: a,d // b,c and
A3: a,d9 // b9,c9;
  b9,c9 // b,c by A1,Th3;
  then a,d // b9,c9 by A2,Def1;
  then a,d // a,d9 by A3,Def1;
  hence thesis by Th4;
end;

theorem
  a,b // a9,b9 & c,d // b,a & c,d9 // b9,a9 implies d = d9
proof
  assume that
A1: a,b // a9,b9 and
A2: c,d // b,a and
A3: c,d9 // b9,a9;
  a9,b9 // a,b by A1,Th3;
  then b9,a9 // b,a by Th7;
  then c,d // b9,a9 by A2,Def1;
  then c,d // c,d9 by A3,Def1;
  hence thesis by Th4;
end;

theorem
  a,b // a9,b9 & c,d // c9,d9 & b,f // c,d & b9,f9 // c9,d9 implies a,f
  // a9,f9
proof
  assume that
A1: a,b // a9,b9 and
A2: c,d // c9,d9 and
A3: b,f // c,d and
A4: b9,f9 // c9,d9;
  b9,f9 // c,d by A2,A4,Def1;
  then
A5: b,f // b9,f9 by A3,Def1;
  b,a // b9,a9 by A1,Th7;
  hence thesis by A5,Def1;
end;

theorem Th12:
  a,b // a9,b9 & a,c // c9,b9 implies b,c // c9,a9
proof
  assume that
A1: a,b // a9,b9 and
A2: a,c // c9,b9;
  consider d such that
A3: c9,b9 // a9,d by Def1;
  a9,d // c9,b9 by A3,Th3;
  then a,c // a9,d by A2,Def1;
  then
A4: b,c // b9,d by A1,Def1;
  c9,a9 // b9,d by A3,Def1;
  hence thesis by A4,Def1;
end;

::
::                  Relation of Maximal Distance
::

definition
  let AFV;
  let a,b;
  pred MDist a,b means

  a,b // b,a & a <> b;
  irreflexivity;
  symmetry by Th3;
end;

theorem
  ex a,b st a<>b & not MDist a,b
proof
  consider p,q such that
A1: p <> q by STRUCT_0:def 10;
  now
    consider r such that
A2: p,r // r,q by Def1;
A3: now
A4:   now
        assume MDist p,r;
        then
A5:     p,r // r,p;
        r,q // p,r by A2,Th3;
        then q,r // r,p by Th7;
        then p,r // q,r by A5,Def1;
        hence thesis by A1,Th4,Th7;
      end;
      assume p <> r;
      hence thesis by A4;
    end;
    now
      assume
A6:   p = r;
      then r,q // p,p by A2,Th3;
      hence thesis by A1,A6,Def1;
    end;
    hence thesis by A3;
  end;
  hence thesis;
end;

theorem
  MDist a,b & MDist a,c implies b = c or MDist b,c
proof
  assume that
A1: MDist a,b and
A2: MDist a,c;
A3: a,b // b,a by A1;
A4: a,c // c,a by A2;
  consider d such that
A5: c,a // b,d by Def1;
  b,d // c,a by A5,Th3;
  then a,c // b,d by A4,Def1;
  then
A6: b,c // a,d by A3,Def1;
  c,b // a,d by A5,Def1;
  then b,c // c,b by A6,Def1;
  hence thesis;
end;

theorem
  MDist a,b & a,b // c,d implies MDist c,d
proof
  assume that
A1: MDist a,b and
A2: a,b // c,d;
A3: a,b // b,a by A1;
A4: c,d // a,b by A2,Th3;
  then d,c // b,a by Th7;
  then d,c // a,b by A3,Def1;
  then c,d // d,c by A4,Def1;
  then c <> d implies thesis;
  hence thesis by A1,A2,Def1;
end;

::
::                        Midpoint Relation
::

definition
  let AFV;
  let a,b,c;
  pred Mid a,b,c means
  :Def3:
  a,b // b,c;
end;

theorem Th16:
  Mid a,b,c implies Mid c,b,a
proof
  assume Mid a,b,c;
  then a,b // b,c;
  then b,a // c,b by Th7;
  then c,b // b,a by Th3;
  hence thesis;
end;

theorem
  Mid a,b,b iff a = b
by Def1,Th6;

theorem Th18:
  Mid a,b,a iff a = b or MDist a,b
by Th6;

theorem Th19:
  ex b st Mid a,b,c
proof
  consider b such that
A1: a,b // b,c by Def1;
  Mid a,b,c by A1;
  hence thesis;
end;

theorem Th20:
  Mid a,b,c & Mid a,b9,c implies b =b9 or MDist b,b9
proof
  assume that
A1: Mid a,b,c and
A2: Mid a,b9,c;
A3: a,b // b,c by A1;
  consider d such that
A4: b9,c // b,d by Def1;
A5: b,d // b9,c by A4,Th3;
  then b,b9 // d,c by Def1;
  then
A6: b9,b // c,d by Th7;
  a,b9 // b9,c by A2;
  then a,b9 // b,d by A5,Def1;
  then b,b9 // c,d by A3,Def1;
  then b,b9 // b9,b by A6,Def1;
  hence thesis;
end;

theorem Th21:
  ex c st Mid a,b,c
proof
  consider c such that
A1: a,b // b,c by Def1;
  Mid a,b,c by A1;
  hence thesis;
end;

theorem Th22:
  Mid a,b,c & Mid a,b,c9 implies c = c9
proof
  assume that
A1: Mid a,b,c and
A2: Mid a,b,c9;
  a,b // b,c9 by A2;
  then
A3: b,c9 // a,b by Th3;
  a,b // b,c by A1;
  then b,c // a,b by Th3;
  then b,c // b,c9 by A3,Def1;
  hence thesis by Th4;
end;

theorem Th23:
  Mid a,b,c & MDist b,b9 implies Mid a,b9,c
proof
  assume that
A1: Mid a,b,c and
A2: MDist b,b9;
A3: b,b9 // b9,b by A2;
  a,b // b,c by A1;
  then
A4: b,a // c,b by Th7;
  consider d such that
A5: b9,b // c,d by Def1;
  c,d // b9,b by A5,Th3;
  then b,b9 // c,d by A3,Def1;
  then
A6: a,b9 // b,d by A4,Def1;
  b9,c // b,d by A5,Def1;
  then a,b9 // b9,c by A6,Def1;
  hence thesis;
end;

theorem Th24:
  Mid a,b,c & Mid a,b9,c9 & MDist b,b9 implies c = c9
proof
  assume that
A1: Mid a,b,c and
A2: Mid a,b9,c9 and
A3: MDist b,b9;
  Mid a,b9,c by A1,A3,Th23;
  hence thesis by A2,Th22;
end;

theorem Th25:
  Mid a,p,a9 & Mid b,p,b9 implies a,b // b9,a9
proof
  assume that
A1: Mid a,p,a9 and
A2: Mid b,p,b9;
  consider d such that
A3: b9,p // a9,d by Def1;
  a,p // p,a9 by A1;
  then
A4: p,a // a9,p by Th7;
  b,p // p,b9 by A2;
  then
A5: p,b // b9,p by Th7;
  a9,d // b9,p by A3,Th3;
  then p,b // a9,d by A5,Def1;
  then
A6: a,b // p,d by A4,Def1;
  b9,a9 // p,d by A3,Def1;
  hence thesis by A6,Def1;
end;

theorem
  Mid a,p,a9 & Mid b,q,b9 & MDist p,q implies a,b // b9,a9
proof
  assume that
A1: Mid a,p,a9 and
A2: Mid b,q,b9 and
A3: MDist p,q;
  Mid a,q,a9 by A1,A3,Th23;
  hence thesis by A2,Th25;
end;

::
::                         Point Symmetry
::

definition
  let AFV;
  let a,b;
  func PSym(a,b) -> Element of AFV means
  :Def4:
  Mid b,a,it;
  correctness by Th21,Th22;
end;

theorem
  PSym(p,a) = b iff a,p // p,b by Def3,Def4;

theorem Th28:
  PSym(p,a) = a iff a = p or MDist a,p
proof
A1: now
    assume a = p or MDist a,p;
    then Mid a,p,a by Th18;
    hence PSym(p,a) = a by Def4;
  end;
  now
    assume PSym(p,a) = a;
    then Mid a,p,a by Def4;
    hence a = p or MDist a,p;
  end;
  hence thesis by A1;
end;

theorem Th29:
  PSym(p,PSym(p,a)) = a
proof
  Mid a,p,PSym(p,a) by Def4;
  then Mid PSym(p,a),p,a by Th16;
  hence thesis by Def4;
end;

theorem Th30:
  PSym(p,a) = PSym(p,b) implies a = b
proof
  assume
A1: PSym(p,a) = PSym(p,b);
  PSym(p,PSym(p,a)) = a by Th29;
  hence thesis by A1,Th29;
end;

theorem
  ex a st PSym(p,a) = b
proof
  PSym(p,PSym(p,b)) = b by Th29;
  hence thesis;
end;

theorem Th32:
  a,b // PSym(p,b),PSym(p,a)
proof
  Mid a,p,PSym(p,a) & Mid b,p,PSym(p,b) by Def4;
  hence thesis by Th25;
end;

theorem Th33:
  a,b // c,d iff PSym(p,a),PSym(p,b) // PSym(p,c),PSym(p,d)
proof
A1: now
    assume
A2: PSym(p,a),PSym(p,b) // PSym(p,c),PSym(p,d);
    d,c // PSym(p,c),PSym(p,d) by Th32;
    then d,c // PSym(p,a),PSym(p,b) by A2,Def1;
    then
A3: c,d // PSym(p,b),PSym(p,a) by Th7;
    a,b // PSym(p,b),PSym(p,a) by Th32;
    hence a,b // c,d by A3,Def1;
  end;
  now
A4: PSym(p,b),PSym(p,a) // a,b by Th3,Th32;
    assume
A5: a,b // c,d;
    PSym(p,d),PSym(p,c) // c,d by Th3,Th32;
    then PSym(p,d),PSym(p,c) // a,b by A5,Def1;
    then PSym(p,b),PSym(p,a) // PSym(p,d),PSym(p,c) by A4,Def1;
    hence PSym(p,a),PSym(p,b) // PSym(p,c),PSym(p,d) by Th7;
  end;
  hence thesis by A1;
end;

theorem
  MDist a,b iff MDist PSym(p,a),PSym(p,b)
by Th30,Th33;

theorem Th35:
  Mid a,b,c iff Mid PSym(p,a),PSym(p,b),PSym(p,c)
by Th33;

theorem Th36:
  PSym(p,a) = PSym(q,a) iff p = q or MDist p,q
proof
A1: now
    assume
A2: MDist p,q;
    Mid a,p,PSym(p,a) & Mid a,q,PSym(q,a) by Def4;
    hence PSym(p,a) = PSym(q,a) by A2,Th24;
  end;
  now
    assume
A3: PSym(p,a) = PSym(q,a);
    Mid a,p,PSym(p,a) & Mid a,q,PSym(q,a) by Def4;
    hence p = q or MDist p,q by A3,Th20;
  end;
  hence thesis by A1;
end;

theorem Th37:
  PSym(q,PSym(p,PSym(q,a))) = PSym(PSym(q,p),a)
proof
  Mid PSym(q,a),p,PSym(p,PSym(q,a)) by Def4;
  then Mid PSym(q,PSym(q,a)),PSym(q,p),PSym(q,PSym(p,PSym(q,a))) by Th35;
  then PSym(q,PSym(p,PSym(q,a)))=PSym(PSym(q,p),PSym(q,PSym(q,a))) by Def4;
  hence thesis by Th29;
end;

theorem
  PSym(p,PSym(q,a)) = PSym(q,PSym(p,a)) iff p = q or MDist p,q or MDist
  q,PSym(p,q)
proof
A1: now
    assume PSym(p,PSym(q,a))=PSym(q,PSym(p,a));
    then PSym(p,PSym(q,PSym(p,a)))=PSym(q,a) by Th29;
    then PSym(PSym(p,q),a)=PSym(q,a) by Th37;
    then q=PSym(p,q) or MDist q,PSym(p,q) by Th36;
    then
A2: Mid q,p,q or MDist q,PSym(p,q) by Def4;
    hence p = q or MDist q,p or MDist q,PSym(p,q);
    thus p = q or MDist p,q or MDist q,PSym(p,q) by A2,Th18;
  end;
  now
    assume p = q or MDist p,q or MDist q,PSym(p,q);
    then Mid q,p,q or MDist q,PSym(p,q) by Th18;
    then PSym(PSym(p,q),a)=PSym(q,a) by Def4,Th36;
    then PSym(p,PSym(q,PSym(p,a)))=PSym(q,a) by Th37;
    hence PSym(p,PSym(q,a))=PSym(q,PSym(p,a)) by Th29;
  end;
  hence thesis by A1;
end;

theorem Th39:
  PSym(p,PSym(q,PSym(r,a))) = PSym(r,PSym(q,PSym(p,a)))
proof
  p,a // PSym(r,a),PSym(r,p) & PSym(q,PSym(r,p)),PSym(q,PSym(r,a)) //
  PSym(r,a ),PSym(r,p) by Th3,Th32;
  then
A1: p,a // PSym(q,PSym(r,p)),PSym(q,PSym(r,a)) by Def1;
  p,a // PSym(p,a),PSym(p,p) & PSym(q,PSym(p,p)),PSym(q,PSym(p,a)) //
  PSym(p,a ),PSym(p,p) by Th3,Th32;
  then
A2: p,a // PSym(q,PSym(p,p)),PSym(q,PSym(p,a)) by Def1;
  PSym(q,p),PSym(r,p) // PSym(r,PSym(r,p)),PSym(r,PSym(q,p)) by Th32;
  then PSym(q,p),PSym(r,p) // p,PSym(r,PSym(q,p)) by Th29;
  then
A3: p,PSym(r,PSym(q,p)) // PSym(q,p),PSym(r,p) by Th3;
  PSym(q,PSym(r,p)),p // PSym(q,p),PSym(q,PSym(q,PSym(r,p))) by Th32;
  then PSym(q,PSym(r,p)),p // PSym(q,p),PSym(r,p) by Th29;
  then PSym(q,PSym(r,p)),p // p,PSym(r,PSym(q,p)) by A3,Def1;
  then Mid PSym(q,PSym(r,p)),p,PSym(r,PSym(q,p));
  then PSym(p,PSym(q,PSym(r,p))) = PSym(r,PSym(q,p)) by Def4;
  then
A4: PSym(p,PSym(q,PSym(r,p))) = PSym(r,PSym(q,PSym(p,p))) by Th28;
  PSym(r,PSym(q,PSym(p,a))),PSym(r,PSym(q,PSym(p,p))) // PSym(q,PSym(p,p)
  ),PSym(q,PSym(p,a)) by Th3,Th32;
  then
A5: PSym(r,PSym(q,PSym(p,a))),PSym(r,PSym(q,PSym(p,p))) // p,a by A2,Def1;
  PSym(p,PSym(q,PSym(r,a))),PSym(p,PSym(q,PSym(r,p))) // PSym(q,PSym(r,p)
  ),PSym(q,PSym(r,a)) by Th3,Th32;
  then PSym(p,PSym(q,PSym(r,a))),PSym(p,PSym(q,PSym(r,p))) // p,a by A1,Def1;
  then PSym(p,PSym(q,PSym(r,a))),PSym(p,PSym(q,PSym(r,p))) // PSym(r,PSym(q,
  PSym(p,a))),PSym(p,PSym(q,PSym(r,p))) by A4,A5,Def1;
  hence thesis by Th4,Th7;
end;

theorem
  ex d st PSym(a,PSym(b,PSym(c,p))) = PSym(d,p)
proof
  consider e such that
A1: Mid a,e,c by Th19;
  consider d such that
A2: Mid b,e,d by Th21;
  c = PSym(e,a) by A1,Def4;
  then PSym(c,PSym(d,p)) = PSym(PSym(e,a),PSym(PSym(e,b),p)) by A2,Def4
    .= PSym(PSym(e,a),PSym(e,PSym(b,PSym(e,p)))) by Th37
    .= PSym(e,PSym(a,PSym(e,PSym(e,PSym(b,PSym(e,p)))))) by Th37
    .= PSym(e,PSym(a,PSym(b,PSym(e,p)))) by Th29
    .= PSym(e,PSym(e,PSym(b,PSym(a,p)))) by Th39
    .= PSym(b,PSym(a,p)) by Th29;
  then PSym(d,p) = PSym(c,PSym(b,PSym(a,p))) by Th29;
  hence thesis by Th39;
end;

theorem
  ex c st PSym(a,PSym(c,p)) = PSym(c,PSym(b,p))
proof
  consider c such that
A1: Mid a,c,b by Th19;
  PSym(b,p) = PSym(PSym(c,a),p) by A1,Def4
    .= PSym(c,PSym(a,(PSym(c,p)))) by Th37;
  then PSym(c,PSym(b,p)) = PSym(a,(PSym(c,p))) by Th29;
  hence thesis;
end;

::
::                     Addition on the carrier
::

definition
  let AFV,o;
  let a,b;
  func Padd(o,a,b) -> Element of AFV means
  :Def5:
  o,a // b,it;
  correctness by Def1,Th5;
end;

notation
  let AFV,o;
  let a;
  synonym Pcom(o,a) for PSym(o,a);
end;

Lm1: Pcom(o,a) = b iff a,o // o,b by Def4,Def3;

definition
  let AFV,o;

  func Padd(o) -> BinOp of the carrier of AFV means
  :Def6:
  for a,b holds it.(a ,b) = Padd(o,a,b);
  existence
  proof
    deffunc F(Element of AFV, Element of AFV) = Padd(o,$1,$2);
    consider O being BinOp of the carrier of AFV such that
A1: for a,b holds O.(a,b) = F(a,b) from BINOP_1:sch 4;
    take O;
    thus thesis by A1;
  end;
  uniqueness
  proof
    set X = the carrier of AFV;
    let o1,o2 be BinOp of the carrier of AFV such that
A2: for a,b holds o1.(a,b) = Padd(o,a,b) and
A3: for a,b holds o2.(a,b) = Padd(o,a,b);
    for x being Element of [:X,X:] holds o1.x = o2.x
    proof
      let x be Element of [:X,X:];
      consider x1,x2 being Element of X such that
A4:   x = [x1,x2] by DOMAIN_1:1;
      o1.x = o1.(x1,x2) by A4
        .= Padd(o,x1,x2) by A2
        .= o2.(x1,x2) by A3
        .= o2.x by A4;
      hence thesis;
    end;
    hence thesis by FUNCT_2:63;
  end;
end;

definition
  let AFV,o;
  func Pcom(o) -> UnOp of the carrier of AFV means
  :Def7:
  for a holds it.a = Pcom(o,a);
  existence
  proof
    deffunc F(Element of AFV) = Pcom(o,$1);
    consider O being UnOp of the carrier of AFV such that
A1: for a holds O.a = F(a) from FUNCT_2:sch 4;
    take O;
    thus thesis by A1;
  end;
  uniqueness
  proof
    set X = the carrier of AFV;
    let o1,o2 be UnOp of the carrier of AFV such that
A2: for a holds o1.a = Pcom(o,a) and
A3: for a holds o2.a = Pcom(o,a);
    for x being Element of X holds o1.x = o2.x
    proof
      let x be Element of X;
      o1.x = Pcom(o,x) by A2
        .= o2.x by A3;
      hence thesis;
    end;
    hence thesis by FUNCT_2:63;
  end;
end;

definition
  let AFV,o;
  func GroupVect(AFV,o) -> strict addLoopStr equals
  addLoopStr(#the carrier of
    AFV,Padd(o),o#);
  correctness;
end;

registration
  let AFV,o;
  cluster GroupVect(AFV,o) -> non empty;
  coherence;
end;

theorem
  the carrier of GroupVect(AFV,o) = the carrier of AFV & the addF of
  GroupVect(AFV,o) = Padd(o) & 0.GroupVect(AFV,o) = o;

reserve a,b,c for Element of GroupVect(AFV,o);

theorem
  for a,b being Element of GroupVect(AFV,o), a9,b9 being Element of AFV
  st a=a9 & b=b9 holds a + b = (Padd(o)).(a9,b9);

Lm2: a+b = b+a
proof
  reconsider a9=a,b9=b as Element of AFV;
  reconsider c9=(a+b) as Element of AFV;
  c9= Padd(o,a9,b9) by Def6;
  then o,a9 // b9,c9 by Def5;
  then o,b9 // a9,c9 by Def1;
  then c9 = Padd(o,b9,a9) by Def5
    .= b + a by Def6;
  hence thesis;
end;

Lm3: (a+b)+c = a+(b+c)
proof
  reconsider a9=a,b9=b,c9=c as Element of AFV;
  set p= b+c,q=a+b;
  reconsider p9=p,q9=q as Element of AFV;
  reconsider x9=(a+p) ,y9=(q+c) as Element of AFV;
  consider x99 such that
A1: x9,p9 // c9,x99 by Def1;
  x9= Padd(o,a9,p9) by Def6;
  then o,a9 // p9,x9 by Def5;
  then
A2: a9,o // x9,p9 by Th7;
  c9,x99 // x9,p9 by A1,Th3;
  then
A3: a9,o // c9,x99 by A2,Def1;
  q9= Padd(o,a9,b9) by Def6;
  then o,a9 // b9,q9 by Def5;
  then o,b9 // a9,q9 by Def1;
  then
A4: a9,q9 // o,b9 by Th3;
  p9= Padd(o,b9,c9) by Def6;
  then o,b9 // c9,p9 by Def5;
  then c9,p9 // o,b9 by Th3;
  then a9,q9 // c9,p9 by A4,Def1;
  then
A5: q9,o // p9,x99 by A3,Def1;
  x9,c9 // p9,x99 by A1,Def1;
  then q9,o // x9,c9 by A5,Def1;
  then o,q9 // c9,x9 by Th7;
  then
A6: c9,x9 // o,q9 by Th3;
  y9= Padd(o,q9,c9) by Def6;
  then o,q9 // c9,y9 by Def5;
  then c9,y9 // o,q9 by Th3;
  then c9,y9 // c9,x9 by A6,Def1;
  hence thesis by Th4;
end;

Lm4: a + (0.(GroupVect(AFV,o))) = a
proof
  reconsider a9=a as Element of AFV;
  reconsider x9=(a + (0.(GroupVect(AFV,o)))) as Element of AFV;
  x9= Padd(o,a9,o) by Def6;
  then o,a9 // o,x9 by Def5;
  hence thesis by Th4;
end;

Lm5: GroupVect(AFV,o) is Abelian add-associative right_zeroed
proof
  thus for a,b holds a+b = b+a by Lm2;
  thus for a,b,c holds (a+b)+c = a+(b+c) by Lm3;
  thus for a holds a + 0.GroupVect(AFV,o) = a by Lm4;
end;

Lm6: GroupVect(AFV,o) is right_complementable
proof
  let s be Element of GroupVect(AFV,o);
  reconsider s9 = s as Element of AFV;
  reconsider t = (Pcom(o)).s9 as Element of GroupVect(AFV,o);
  take t;
  Pcom(o,o) = o by Th28;
  then o,s9 // Pcom(o,s9),o by Th32;
  then
A1: Padd(o,s9,Pcom(o,s9)) = o by Def5;
  thus s + t = (Padd(o)).(s9,(Pcom(o,s9))) by Def7
    .= 0.GroupVect(AFV,o) by A1,Def6;
end;

registration
  let AFV,o;
  cluster GroupVect(AFV,o) -> Abelian add-associative right_zeroed
    right_complementable;
  coherence by Lm5,Lm6;
end;

theorem Th44:
  for a being Element of GroupVect(AFV,o), a9 being Element of AFV
  st a=a9 holds -a = (Pcom(o)).a9
proof
  let a be Element of GroupVect(AFV,o), a9 be Element of AFV;
  assume
A1: a=a9;
  reconsider aa = (Pcom(o)).a9 as Element of GroupVect(AFV,o);
  Pcom(o,o) = o & o,a9 // Pcom(o,a9),Pcom(o,o) by Th28,Th32;
  then
A2: Padd(o,a9,Pcom(o,a9)) = o by Def5;
  a + aa = (Padd(o)).(a,(Pcom(o,a9))) by Def7
    .= 0.GroupVect(AFV,o) by A1,A2,Def6;
  hence thesis by RLVECT_1:def 10;
end;

theorem
  0.GroupVect(AFV,o) = o;

reserve a,b for Element of GroupVect(AFV,o);

theorem Th46:
  for a ex b st b + b = a
proof
  let a;
  reconsider a99=a as Element of AFV;
  consider b9 being Element of AFV such that
A1: o,b9 // b9,a99 by Def1;
  reconsider b=b9 as Element of GroupVect(AFV,o);
  a99 = Padd(o,b9,b9) by A1,Def5
    .= b+b by Def6;
  hence thesis;
end;

registration
  let AFV,o;
  cluster GroupVect(AFV,o) -> Two_Divisible;
  coherence
  proof
    for a ex b st b + b = a by Th46;
    hence thesis by TDGROUP:def 1;
  end;
end;

::
::        Representation Theorem for Directed Geometrical Bundles
::

reserve AFV for AffVect,
  o for Element of AFV;

theorem Th47:
  for a being Element of GroupVect(AFV,o) st a + a = 0.(GroupVect(
  AFV,o)) holds a = 0.(GroupVect(AFV,o))
proof
  let a be Element of GroupVect(AFV,o) such that
A1: a + a = 0.(GroupVect(AFV,o));
  reconsider a99=a as Element of AFV;
  o = Padd(o,a99,a99) by A1,Def6;
  then
A2: o,a99 // a99,o by Def5;
  o,o // o,o by Th1;
  hence thesis by A2,TDGROUP:16;
end;

registration
  let AFV,o;
  cluster GroupVect(AFV,o) -> Fanoian;
  coherence
  proof
    for a being Element of GroupVect(AFV,o) st a + a = 0.(GroupVect(AFV,o)
    ) holds a = 0.(GroupVect(AFV,o)) by Th47;
    hence thesis by VECTSP_1:def 18;
  end;
end;

registration
  cluster strict non trivial for Uniquely_Two_Divisible_Group;
  existence
  proof
    set X = G_Real;
    X is non trivial by TDGROUP:6;
    hence thesis;
  end;
end;

definition
  mode Proper_Uniquely_Two_Divisible_Group is non trivial
    Uniquely_Two_Divisible_Group;
end;

theorem
  GroupVect(AFV,o) is Proper_Uniquely_Two_Divisible_Group;

registration
  let AFV,o;
  cluster GroupVect(AFV,o) -> non trivial;
  coherence;
end;

theorem Th49:
  for ADG being Proper_Uniquely_Two_Divisible_Group holds AV(ADG) is AffVect
proof
  let ADG be Proper_Uniquely_Two_Divisible_Group;
  ex a,b being Element of ADG st a<>b by STRUCT_0:def 10;
  hence thesis by TDGROUP:17;
end;

registration
  let ADG be Proper_Uniquely_Two_Divisible_Group;
  cluster AV(ADG) -> AffVect-like non trivial;
  coherence by Th49;
end;

theorem Th50:
  for AFV being strict AffVect holds for o being Element of AFV
  holds AFV = AV(GroupVect(AFV,o))
proof
  let AFV be strict AffVect;
  let o be Element of AFV;
  set X = GroupVect(AFV,o);
  now
    let x,y be object;
    set xy = [x,y];
A1: now
      set V = the carrier of AFV;
      assume
A2:   xy in the CONGR of AFV;
      set VV = [:V,V:];
      xy`2 = y;
      then
A3:   y in VV by A2,MCART_1:10;
      then
A4:   y = [y`1,y`2] by MCART_1:21;
      xy`1 = x;
      then
A5:   x in VV by A2,MCART_1:10;
      then reconsider
      x1 = x`1, x2 = x`2, y1 = y`1, y2 = y`2 as Element of AFV by A3,MCART_1:10
;
      reconsider x19 = x1, x29 = x2, y19 = y1, y29 = y2 as Element of X;
A6:   x = [x`1,x`2] by A5,MCART_1:21;
      then
A7:   x1,x2 // y1,y2 by A2,A4,ANALOAF:def 2;
      x19 # y29 = x29 # y19
      proof
        reconsider z1=x19#y29,z2=x29#y19 as Element of AFV;
        z1 = Padd(o,x1,y2) by Def6;
        then o,x1 // y2,z1 by Def5;
        then x1,o // z1,y2 by Th7;
        then
A8:     o,x2 // y1,z1 by A7,Th12;
        z2 = Padd(o,x2,y1) by Def6;
        hence thesis by A8,Def5;
      end;
      hence [x,y] in CONGRD(X) by A6,A4,TDGROUP:def 2;
    end;
    now
      set V = the carrier of X;
      assume
A9:   xy in CONGRD(X);
      set VV = [:V,V:];
      xy`2 = y;
      then
A10:  y in VV by A9,MCART_1:10;
      then
A11:  y = [y`1,y`2] by MCART_1:21;
      xy`1 = x;
      then
A12:  x in VV by A9,MCART_1:10;
      then reconsider
      x19 = x`1, x29 = x`2, y19 = y`1, y29 = y`2 as Element of X by A10,
MCART_1:10;
      set z19 = x19 # y29, z29 = x29 # y19;
      reconsider x1 = x19, x2 = x29, y1 = y19, y2 = y29 as Element of AFV;
      reconsider z1=z19,z2=z29 as Element of AFV;
A13:  z2 = Padd(o,x2,y1) by Def6;
      z1 = Padd(o,x1,y2) by Def6;
      then
A14:  o,x1 // y2,z1 by Def5;
A15:  x = [x`1,x`2] by A12,MCART_1:21;
      then z19=z29 by A9,A11,TDGROUP:def 2;
      then o,x2 // y1,z1 by A13,Def5;
      then x1,x2 // y1,y2 by A14,Th12;
      hence xy in the CONGR of AFV by A15,A11,ANALOAF:def 2;
    end;
    hence [x,y] in CONGRD(X) iff [x,y] in the CONGR of AFV by A1;
  end;
  then the carrier of AV(X) = the carrier of AFV & CONGRD(X) = the CONGR of
  AFV by RELAT_1:def 2,TDGROUP:4;
  hence thesis by TDGROUP:4;
end;

theorem
  for AS being strict AffinStruct holds (AS is AffVect iff ex ADG being
  Proper_Uniquely_Two_Divisible_Group st AS = AV(ADG) )
proof
  let AS be strict AffinStruct;
  now
    assume AS is AffVect;
    then reconsider AS9 = AS as AffVect;
    set o = the Element of AS9;
    take ADG = GroupVect(AS9,o);
    AS9 = AV(ADG) by Th50;
    hence ex ADG being Proper_Uniquely_Two_Divisible_Group st AS = AV(ADG);
  end;
  hence thesis;
end;

definition
  let X,Y be non empty addLoopStr;
  let f be Function of the carrier of X,the carrier of Y;
  pred f is_Iso_of X,Y means

  f is one-to-one & rng(f) = the carrier of
Y & for a,b being Element of X holds f.(a+b) = (f.a)+(f.b) & f.(0.X) = 0.Y & f.
  (-a) = -(f.a);
end;

definition
  let X,Y be non empty addLoopStr;
  pred X,Y are_Iso means

  ex f being Function of the carrier of X,the carrier of Y st f is_Iso_of X,Y;
end;

reserve ADG for Proper_Uniquely_Two_Divisible_Group;
reserve f for Function of the carrier of ADG,the carrier of ADG;

theorem Th52:
  for o9 being Element of ADG, o being Element of AV(ADG) st (for
x being Element of ADG holds f.x = o9+x) & o=o9 holds for a,b being Element of
ADG holds f.(a+b) =(Padd(o)).(f.a,f.b) & f.(0.ADG) = 0.(GroupVect(AV(ADG),o)) &
  f.(-a) = (Pcom(o)).(f.a)
proof
  let o9 be Element of ADG, o be Element of AV(ADG);
  assume that
A1: for x being Element of ADG holds f.x = o9+x and
A2: o=o9;
  let a,b be Element of ADG;
  set a9=f.a,b9=f.b;
A3: AV(ADG) = AffinStruct(#the carrier of ADG,CONGRD(ADG)#) by TDGROUP:def 3;
  then reconsider a99=a9,b99=b9 as Element of AV(ADG);
  thus f.(a+b) =(Padd(o)).((f.a),(f.b))
  proof
A4: ((Padd(o)).((f.a),(f.b))) = Padd(o,a99,b99) by Def6;
    then reconsider c99= (Padd(o)).((f.a),(f.b)) as Element of AV( ADG);
    reconsider c9=c99 as Element of ADG by A3;
    o,a99 // b99,c99 by A4,Def5;
    then [[o9,a9],[b9,c9]] in CONGRD(ADG) by A2,A3,ANALOAF:def 2;
    then
A5: o9+c9 = a9+b9 by TDGROUP:def 2;
    a9 = o9+a & b9 = o9+b by A1;
    then o9+c9 = (o9+((a+o9)+b)) by A5,RLVECT_1:def 3
      .= o9+(o9+(a+b)) by RLVECT_1:def 3;
    then c9 = o9+(a+b) by RLVECT_1:8
      .= f.(a+b) by A1;
    hence thesis;
  end;
  f.(0.ADG) = o9+(0.ADG) by A1
    .= 0.(GroupVect(AV(ADG),o)) by A2,RLVECT_1:4;
  hence f.(0.ADG) = 0.(GroupVect(AV(ADG),o));
  thus f.(-a) = (Pcom(o)).(f.a)
  proof
A6: ((Pcom(o)).(f.a)) = Pcom(o,a99) by Def7;
    then reconsider c99 = (Pcom(o)).(f.a) as Element of AV(ADG);
    reconsider c9=c99 as Element of ADG by A3;
    a99,o // o,c99 by A6,Lm1;
    then [[a9,o9],[o9,c9]] in CONGRD(ADG) by A2,A3,ANALOAF:def 2;
    then a9+c9 = o9+o9 by TDGROUP:def 2;
    then
A7: o9+o9 = (o9+a)+c9 by A1
      .= o9+(a+c9) by RLVECT_1:def 3;
    f.(-a) = o9+(-a) by A1
      .= (c9+a)+(-a) by A7,RLVECT_1:8
      .= c9+(a+(-a)) by RLVECT_1:def 3
      .= c9+(0.ADG) by RLVECT_1:5
      .= c9 by RLVECT_1:4;
    hence thesis;
  end;
end;

theorem Th53:
  for o9 being Element of ADG st (for b being Element of ADG holds
  f.b = o9+b) holds f is one-to-one
proof
  let o9 be Element of ADG such that
A1: for b being Element of ADG holds f.b = o9+b;
  now
    let x1,x2 be object such that
A2: x1 in dom(f) & x2 in dom(f) and
A3: f.x1 = f.x2;
    reconsider x19=x1,x29=x2 as Element of ADG by A2,FUNCT_2:def 1;
    o9+x29 = f.x19 by A1,A3
      .= o9+x19 by A1;
    hence x1=x2 by RLVECT_1:8;
  end;
  hence thesis by FUNCT_1:def 4;
end;

theorem Th54:
  for o9 being Element of ADG, o being Element of AV(ADG) st (for
  b being Element of ADG holds f.b = o9+b) holds rng(f) = the carrier of
  GroupVect(AV(ADG),o)
proof
  set X = the carrier of ADG;
A1: X = dom(f) by FUNCT_2:def 1;
  let o9 be Element of ADG, o be Element of AV(ADG) such that
A2: for b being Element of ADG holds f.b = o9+b;
  now
    let y be object;
    assume y in X;
    then reconsider y9=y as Element of X;
    set x9=y9-o9;
    f.x9 = o9+((-o9)+y9) by A2
      .= (o9+(-o9))+y9 by RLVECT_1:def 3
      .= y9+(0.ADG) by RLVECT_1:5
      .= y by RLVECT_1:4;
    hence y in rng(f) by A1,FUNCT_1:def 3;
  end;
  then
A3: X c= rng(f) by TARSKI:def 3;
  rng(f) c= X & X = the carrier of GroupVect(AV(ADG),o) by RELAT_1:def 19
,TDGROUP:4;
  hence thesis by A3,XBOOLE_0:def 10;
end;

theorem
  for ADG being Proper_Uniquely_Two_Divisible_Group, o9 being Element of
ADG, o being Element of AV(ADG) st o=o9 holds ADG,GroupVect(AV(ADG),o) are_Iso
proof
  let ADG be Proper_Uniquely_Two_Divisible_Group, o9 be Element of ADG, o be
  Element of AV(ADG) such that
A1: o=o9;
  set AS = AV(ADG);
  set X = the carrier of ADG,Z=GroupVect(AS,o);
  set T = the carrier of GroupVect(AS,o);
  deffunc F(Element of X) = o9+$1;
  consider g being UnOp of X such that
A2: for a being Element of X holds g.a = F(a) from FUNCT_2:sch 4;
  X = T by TDGROUP:4;
  then reconsider f = g as Function of X,T;
A3: now
    let a,b be Element of ADG;
    reconsider fa = f.a as Element of AV(ADG);
    thus f.(a+b) = (f.a)+(f.b) by A1,A2,Th52;
    thus f.(0.ADG) = 0.Z by A1,A2,Th52;
    thus f.(-a) = (Pcom(o)).fa by A1,A2,Th52
      .= -(f.a) by Th44;
  end;
  f is one-to-one & rng(f) = T by A2,Th53,Th54;
  then f is_Iso_of ADG,Z by A3;
  hence thesis;
end;