:: AFVECT0 semantic presentation

begin

definition
let IT be non empty AffinStruct ;
attrIT is WeakAffVect-like  means :Def1: :: AFVECT0:def 1
( ( 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;

:: deftheorem Def1 defines WeakAffVect-like AFVECT0:def_1_:_
 for IT being non empty AffinStruct holds
( IT is WeakAffVect-like iff ( ( 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 ) ) );

registration
cluster non empty non trivial strict WeakAffVect-like for AffinStruct ;
existence
 ex b1 being non trivial AffinStruct st
( b1 is strict & b1 is WeakAffVect-like )
proof
set AFV = the strict AffVect;
reconsider AS = the strict AffVect 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, Def1;
hence  ex b1 being non trivial AffinStruct st
( b1 is strict & b1 is WeakAffVect-like ) ; ::_thesis: verum
end;
end;

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

registration
cluster non empty AffVect-like  ->  non empty WeakAffVect-like for AffinStruct ;
coherence
 for b1 being non empty AffinStruct st b1 is AffVect-like holds
b1 is WeakAffVect-like
proof
let AFV be non empty AffinStruct ; ::_thesis: ( AFV is AffVect-like implies AFV is WeakAffVect-like )
assume A1: AFV is AffVect-like ; ::_thesis: AFV is WeakAffVect-like
A2: ( ( for a, b, c being Element of AFV ex d being Element of AFV st a,b // c,d ) & ( for a, b, c, a9, b9, c9 being Element of AFV st a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9 ) ) by A1, TDGROUP:def_5;
A3: ( ( for a, c being Element of AFV ex b being Element of AFV st a,b // b,c ) & ( for a, b, c, d being Element of AFV st a,b // c,d holds
a,c // b,d ) ) by A1, TDGROUP:def_5;
 ( ( for a, b, c being Element of AFV st a,b // c,c holds
a = b ) & ( for a, b, c, d, p, q being Element of AFV st a,b // p,q & c,d // p,q holds
a,b // c,d ) ) by A1, TDGROUP:def_5;
hence  AFV is WeakAffVect-like by A2, A3, Def1; ::_thesis: verum
end;
end;


theorem Th1: :: AFVECT0:1
for AFV being WeakAffVect
for a, b being Element of AFV holds a,b // a,b
proof
let AFV be WeakAffVect; ::_thesis: for a, b being Element of AFV holds a,b // a,b
let a, b be Element of AFV; ::_thesis: a,b // a,b
 ex d being Element of AFV st a,b // b,d by Def1;
hence  a,b // a,b by Def1; ::_thesis: verum
end;

theorem :: AFVECT0:2
for AFV being WeakAffVect
for a being Element of AFV holds a,a // a,a by Th1;

theorem Th3: :: AFVECT0:3
for AFV being WeakAffVect
for a, b, c, d being Element of AFV st a,b // c,d holds
c,d // a,b
proof
let AFV be WeakAffVect; ::_thesis: for a, b, c, d being Element of AFV st a,b // c,d holds
c,d // a,b
let a, b, c, d be Element of AFV; ::_thesis: ( a,b // c,d implies c,d // a,b )
assume A1: a,b // c,d ; ::_thesis: c,d // a,b
 c,d // c,d by Th1;
hence  c,d // a,b by A1, Def1; ::_thesis: verum
end;

theorem Th4: :: AFVECT0:4
for AFV being WeakAffVect
for a, b, c being Element of AFV st a,b // a,c holds
b = c
proof
let AFV be WeakAffVect; ::_thesis: for a, b, c being Element of AFV st a,b // a,c holds
b = c
let a, b, c be Element of AFV; ::_thesis: ( a,b // a,c implies b = c )
assume  a,b // a,c ; ::_thesis: b = c
then  a,a // b,c by Def1;
then  b,c // a,a by Th3;
hence  b = c by Def1; ::_thesis: verum
end;

theorem Th5: :: AFVECT0:5
for AFV being WeakAffVect
for a, b, c, d, d9 being Element of AFV st a,b // c,d & a,b // c,d9 holds
d = d9
proof
let AFV be WeakAffVect; ::_thesis: for a, b, c, d, d9 being Element of AFV st a,b // c,d & a,b // c,d9 holds
d = d9
let a, b, c, d, d9 be Element of AFV; ::_thesis: ( a,b // c,d & a,b // c,d9 implies d = d9 )
assume  ( a,b // c,d & a,b // c,d9 ) ; ::_thesis: d = d9
then  ( c,d // a,b & c,d9 // a,b ) by Th3;
then  c,d // c,d9 by Def1;
hence  d = d9 by Th4; ::_thesis: verum
end;

theorem Th6: :: AFVECT0:6
for AFV being WeakAffVect
for a, b being Element of AFV holds a,a // b,b
proof
let AFV be WeakAffVect; ::_thesis: for a, b being Element of AFV holds a,a // b,b
let a, b be Element of AFV; ::_thesis: a,a // b,b
consider p being Element of AFV such that
A1: a,a // b,p by Def1;
 b,p // a,a by A1, Th3;
hence  a,a // b,b by A1, Def1; ::_thesis: verum
end;

theorem Th7: :: AFVECT0:7
for AFV being WeakAffVect
for a, b, c, d being Element of AFV st a,b // c,d holds
b,a // d,c
proof
let AFV be WeakAffVect; ::_thesis: for a, b, c, d being Element of AFV st a,b // c,d holds
b,a // d,c
let a, b, c, d be Element of AFV; ::_thesis: ( a,b // c,d implies b,a // d,c )
assume A1: a,b // c,d ; ::_thesis: b,a // d,c
 a,a // c,c by Th6;
hence  b,a // d,c by A1, Def1; ::_thesis: verum
end;

theorem :: AFVECT0:8
for AFV being WeakAffVect
for a, b, c, d, b9 being Element of AFV st a,b // c,d & a,c // b9,d holds
b = b9
proof
let AFV be WeakAffVect; ::_thesis: for a, b, c, d, b9 being Element of AFV st a,b // c,d & a,c // b9,d holds
b = b9
let a, b, c, d, b9 be Element of AFV; ::_thesis: ( a,b // c,d & a,c // b9,d implies b = b9 )
assume that
A1: a,b // c,d and
A2: a,c // b9,d ; ::_thesis: b = b9
 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  b = b9 by Th4; ::_thesis: verum
end;

theorem :: AFVECT0:9
for AFV being WeakAffVect
for b, c, b9, c9, a, d, d9 being Element of AFV st b,c // b9,c9 & a,d // b,c & a,d9 // b9,c9 holds
d = d9
proof
let AFV be WeakAffVect; ::_thesis: for b, c, b9, c9, a, d, d9 being Element of AFV st b,c // b9,c9 & a,d // b,c & a,d9 // b9,c9 holds
d = d9
let b, c, b9, c9, a, d, d9 be Element of AFV; ::_thesis: ( b,c // b9,c9 & a,d // b,c & a,d9 // b9,c9 implies d = d9 )
assume that
A1: b,c // b9,c9 and
A2: a,d // b,c and
A3: a,d9 // b9,c9 ; ::_thesis: d = d9
 b9,c9 // b,c by A1, Th3;
then  a,d // b9,c9 by A2, Def1;
then  a,d // a,d9 by A3, Def1;
hence  d = d9 by Th4; ::_thesis: verum
end;

theorem :: AFVECT0:10
for AFV being WeakAffVect
for a, b, a9, b9, c, d, d9 being Element of AFV st a,b // a9,b9 & c,d // b,a & c,d9 // b9,a9 holds
d = d9
proof
let AFV be WeakAffVect; ::_thesis: for a, b, a9, b9, c, d, d9 being Element of AFV st a,b // a9,b9 & c,d // b,a & c,d9 // b9,a9 holds
d = d9
let a, b, a9, b9, c, d, d9 be Element of AFV; ::_thesis: ( a,b // a9,b9 & c,d // b,a & c,d9 // b9,a9 implies d = d9 )
assume that
A1: a,b // a9,b9 and
A2: c,d // b,a and
A3: c,d9 // b9,a9 ; ::_thesis: d = d9
 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  d = d9 by Th4; ::_thesis: verum
end;

theorem :: AFVECT0:11
for AFV being WeakAffVect
for a, b, a9, b9, c, d, c9, d9, f, f9 being Element of AFV st a,b // a9,b9 & c,d // c9,d9 & b,f // c,d & b9,f9 // c9,d9 holds
a,f // a9,f9
proof
let AFV be WeakAffVect; ::_thesis: for a, b, a9, b9, c, d, c9, d9, f, f9 being Element of AFV st a,b // a9,b9 & c,d // c9,d9 & b,f // c,d & b9,f9 // c9,d9 holds
a,f // a9,f9
let a, b, a9, b9, c, d, c9, d9, f, f9 be Element of AFV; ::_thesis: ( a,b // a9,b9 & c,d // c9,d9 & b,f // c,d & b9,f9 // c9,d9 implies a,f // a9,f9 )
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 ; ::_thesis: a,f // a9,f9
 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  a,f // a9,f9 by A5, Def1; ::_thesis: verum
end;

theorem Th12: :: AFVECT0:12
for AFV being WeakAffVect
for a, b, a9, b9, c, c9 being Element of AFV st a,b // a9,b9 & a,c // c9,b9 holds
b,c // c9,a9
proof
let AFV be WeakAffVect; ::_thesis: for a, b, a9, b9, c, c9 being Element of AFV st a,b // a9,b9 & a,c // c9,b9 holds
b,c // c9,a9
let a, b, a9, b9, c, c9 be Element of AFV; ::_thesis: ( a,b // a9,b9 & a,c // c9,b9 implies b,c // c9,a9 )
assume that
A1: a,b // a9,b9 and
A2: a,c // c9,b9 ; ::_thesis: b,c // c9,a9
consider d being Element of AFV 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  b,c // c9,a9 by A4, Def1; ::_thesis: verum
end;

definition
let AFV be WeakAffVect;
let a, b be Element of AFV;
pred MDist a,b means :Def2: :: AFVECT0:def 2
( a,b // b,a & a <> b );
irreflexivity
 for a being Element of AFV holds
( not a,a // a,a or not a <> a ) ;
symmetry
 for a, b being Element of AFV st a,b // b,a & a <> b holds
( b,a // a,b & b <> a ) by Th3;
end;

:: deftheorem Def2 defines MDist AFVECT0:def_2_:_
 for AFV being WeakAffVect
for a, b being Element of AFV holds
( MDist a,b iff ( a,b // b,a & a <> b ) );

theorem :: AFVECT0:13
for AFV being WeakAffVect ex a, b being Element of AFV st
( a <> b & not MDist a,b )
proof
let AFV be WeakAffVect; ::_thesis: ex a, b being Element of AFV st
( a <> b & not MDist a,b )
consider p, q being Element of AFV such that
A1: p <> q by STRUCT_0:def_10;
now__::_thesis:_ex_a,_b_being_Element_of_AFV_st_
(_a_<>_b_&_not_MDist_a,b_)
consider r being Element of AFV such that
A2: p,r // r,q by Def1;
A3: now__::_thesis:_(_p_<>_r_implies_ex_a,_b_being_Element_of_AFV_st_
(_a_<>_b_&_not_MDist_a,b_)_)
A4: now__::_thesis:_(_MDist_p,r_implies_ex_a,_b_being_Element_of_AFV_st_
(_a_<>_b_&_not_MDist_a,b_)_)
assume  MDist p,r ; ::_thesis: ex a, b being Element of AFV st
( a <> b & not MDist a,b )
then A5: p,r // r,p by Def2;
 r,q // p,r by A2, Th3;
then  q,r // r,p by Th7;
then  p,r // q,r by A5, Def1;
hence  ex a, b being Element of AFV st
( a <> b & not MDist a,b ) by A1, Th4, Th7; ::_thesis: verum
end;
assume  p <> r ; ::_thesis: ex a, b being Element of AFV st
( a <> b & not MDist a,b )
hence  ex a, b being Element of AFV st
( a <> b & not MDist a,b ) by A4; ::_thesis: verum
end;
now__::_thesis:_(_p_=_r_implies_ex_a,_b_being_Element_of_AFV_st_
(_a_<>_b_&_not_MDist_a,b_)_)
assume A6: p = r ; ::_thesis: ex a, b being Element of AFV st
( a <> b & not MDist a,b )
then  r,q // p,p by A2, Th3;
hence  ex a, b being Element of AFV st
( a <> b & not MDist a,b ) by A1, A6, Def1; ::_thesis: verum
end;
hence  ex a, b being Element of AFV st
( a <> b & not MDist a,b ) by A3; ::_thesis: verum
end;
hence  ex a, b being Element of AFV st
( a <> b & not MDist a,b ) ; ::_thesis: verum
end;

theorem :: AFVECT0:14
for AFV being WeakAffVect
for a, b, c being Element of AFV st MDist a,b & MDist a,c & not b = c holds
MDist b,c
proof
let AFV be WeakAffVect; ::_thesis: for a, b, c being Element of AFV st MDist a,b & MDist a,c & not b = c holds
MDist b,c
let a, b, c be Element of AFV; ::_thesis: ( MDist a,b & MDist a,c & not b = c implies MDist b,c )
assume that
A1: MDist a,b and
A2: MDist a,c ; ::_thesis: ( b = c or MDist b,c )
A3: a,b // b,a by A1, Def2;
A4: a,c // c,a by A2, Def2;
consider d being Element of AFV 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  ( b = c or MDist b,c ) by Def2; ::_thesis: verum
end;

theorem :: AFVECT0:15
for AFV being WeakAffVect
for a, b, c, d being Element of AFV st MDist a,b & a,b // c,d holds
MDist c,d
proof
let AFV be WeakAffVect; ::_thesis: for a, b, c, d being Element of AFV st MDist a,b & a,b // c,d holds
MDist c,d
let a, b, c, d be Element of AFV; ::_thesis: ( MDist a,b & a,b // c,d implies MDist c,d )
assume that
A1: MDist a,b and
A2: a,b // c,d ; ::_thesis: MDist c,d
A3: a,b // b,a by A1, Def2;
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 MDist c,d ) by Def2;
hence  MDist c,d by A1, A2, Def1; ::_thesis: verum
end;

definition
let AFV be WeakAffVect;
let a, b, c be Element of AFV;
pred Mid a,b,c means :Def3: :: AFVECT0:def 3
a,b // b,c;
end;

:: deftheorem Def3 defines Mid AFVECT0:def_3_:_
 for AFV being WeakAffVect
for a, b, c being Element of AFV holds
( Mid a,b,c iff a,b // b,c );

theorem Th16: :: AFVECT0:16
for AFV being WeakAffVect
for a, b, c being Element of AFV st Mid a,b,c holds
Mid c,b,a
proof
let AFV be WeakAffVect; ::_thesis: for a, b, c being Element of AFV st Mid a,b,c holds
Mid c,b,a
let a, b, c be Element of AFV; ::_thesis: ( Mid a,b,c implies Mid c,b,a )
assume  Mid a,b,c ; ::_thesis: Mid c,b,a
then  a,b // b,c by Def3;
then  b,a // c,b by Th7;
then  c,b // b,a by Th3;
hence  Mid c,b,a by Def3; ::_thesis: verum
end;

theorem :: AFVECT0:17
for AFV being WeakAffVect
for a, b being Element of AFV holds
( Mid a,b,b iff a = b )
proof
let AFV be WeakAffVect; ::_thesis: for a, b being Element of AFV holds
( Mid a,b,b iff a = b )
let a, b be Element of AFV; ::_thesis: ( Mid a,b,b iff a = b )
A1: now__::_thesis:_(_a_=_b_implies_Mid_a,b,b_)
assume  a = b ; ::_thesis: Mid a,b,b
then  a,b // b,b by Th6;
hence  Mid a,b,b by Def3; ::_thesis: verum
end;
now__::_thesis:_(_Mid_a,b,b_implies_a_=_b_)
assume  Mid a,b,b ; ::_thesis: a = b
then  a,b // b,b by Def3;
hence  a = b by Def1; ::_thesis: verum
end;
hence  ( Mid a,b,b iff a = b ) by A1; ::_thesis: verum
end;

theorem Th18: :: AFVECT0:18
for AFV being WeakAffVect
for a, b being Element of AFV holds
( Mid a,b,a iff ( a = b or MDist a,b ) )
proof
let AFV be WeakAffVect; ::_thesis: for a, b being Element of AFV holds
( Mid a,b,a iff ( a = b or MDist a,b ) )
let a, b be Element of AFV; ::_thesis: ( Mid a,b,a iff ( a = b or MDist a,b ) )
A1: now__::_thesis:_(_a_=_b_implies_Mid_a,b,a_)
assume  a = b ; ::_thesis: Mid a,b,a
then  a,b // b,a by Th6;
hence  Mid a,b,a by Def3; ::_thesis: verum
end;
A2: now__::_thesis:_(_MDist_a,b_implies_Mid_a,b,a_)
assume  MDist a,b ; ::_thesis: Mid a,b,a
then  a,b // b,a by Def2;
hence  Mid a,b,a by Def3; ::_thesis: verum
end;
now__::_thesis:_(_not_Mid_a,b,a_or_a_=_b_or_MDist_a,b_)
assume  Mid a,b,a ; ::_thesis: ( a = b or MDist a,b )
then  a,b // b,a by Def3;
hence  ( a = b or MDist a,b ) by Def2; ::_thesis: verum
end;
hence  ( Mid a,b,a iff ( a = b or MDist a,b ) ) by A1, A2; ::_thesis: verum
end;

theorem Th19: :: AFVECT0:19
for AFV being WeakAffVect
for a, c being Element of AFV ex b being Element of AFV st Mid a,b,c
proof
let AFV be WeakAffVect; ::_thesis: for a, c being Element of AFV ex b being Element of AFV st Mid a,b,c
let a, c be Element of AFV; ::_thesis: ex b being Element of AFV st Mid a,b,c
consider b being Element of AFV such that
A1: a,b // b,c by Def1;
 Mid a,b,c by A1, Def3;
hence  ex b being Element of AFV st Mid a,b,c ; ::_thesis: verum
end;

theorem Th20: :: AFVECT0:20
for AFV being WeakAffVect
for a, b, c, b9 being Element of AFV st Mid a,b,c & Mid a,b9,c & not b = b9 holds
MDist b,b9
proof
let AFV be WeakAffVect; ::_thesis: for a, b, c, b9 being Element of AFV st Mid a,b,c & Mid a,b9,c & not b = b9 holds
MDist b,b9
let a, b, c, b9 be Element of AFV; ::_thesis: ( Mid a,b,c & Mid a,b9,c & not b = b9 implies MDist b,b9 )
assume that
A1: Mid a,b,c and
A2: Mid a,b9,c ; ::_thesis: ( b = b9 or MDist b,b9 )
A3: a,b // b,c by A1, Def3;
consider d being Element of AFV 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, Def3;
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  ( b = b9 or MDist b,b9 ) by Def2; ::_thesis: verum
end;

theorem Th21: :: AFVECT0:21
for AFV being WeakAffVect
for a, b being Element of AFV ex c being Element of AFV st Mid a,b,c
proof
let AFV be WeakAffVect; ::_thesis: for a, b being Element of AFV ex c being Element of AFV st Mid a,b,c
let a, b be Element of AFV; ::_thesis: ex c being Element of AFV st Mid a,b,c
consider c being Element of AFV such that
A1: a,b // b,c by Def1;
 Mid a,b,c by A1, Def3;
hence  ex c being Element of AFV st Mid a,b,c ; ::_thesis: verum
end;

theorem Th22: :: AFVECT0:22
for AFV being WeakAffVect
for a, b, c, c9 being Element of AFV st Mid a,b,c & Mid a,b,c9 holds
c = c9
proof
let AFV be WeakAffVect; ::_thesis: for a, b, c, c9 being Element of AFV st Mid a,b,c & Mid a,b,c9 holds
c = c9
let a, b, c, c9 be Element of AFV; ::_thesis: ( Mid a,b,c & Mid a,b,c9 implies c = c9 )
assume that
A1: Mid a,b,c and
A2: Mid a,b,c9 ; ::_thesis: c = c9
 a,b // b,c9 by A2, Def3;
then A3: b,c9 // a,b by Th3;
 a,b // b,c by A1, Def3;
then  b,c // a,b by Th3;
then  b,c // b,c9 by A3, Def1;
hence  c = c9 by Th4; ::_thesis: verum
end;

theorem Th23: :: AFVECT0:23
for AFV being WeakAffVect
for a, b, c, b9 being Element of AFV st Mid a,b,c & MDist b,b9 holds
Mid a,b9,c
proof
let AFV be WeakAffVect; ::_thesis: for a, b, c, b9 being Element of AFV st Mid a,b,c & MDist b,b9 holds
Mid a,b9,c
let a, b, c, b9 be Element of AFV; ::_thesis: ( Mid a,b,c & MDist b,b9 implies Mid a,b9,c )
assume that
A1: Mid a,b,c and
A2: MDist b,b9 ; ::_thesis: Mid a,b9,c
A3: b,b9 // b9,b by A2, Def2;
 a,b // b,c by A1, Def3;
then A4: b,a // c,b by Th7;
consider d being Element of AFV 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  Mid a,b9,c by Def3; ::_thesis: verum
end;

theorem Th24: :: AFVECT0:24
for AFV being WeakAffVect
for a, b, c, b9, c9 being Element of AFV st Mid a,b,c & Mid a,b9,c9 & MDist b,b9 holds
c = c9
proof
let AFV be WeakAffVect; ::_thesis: for a, b, c, b9, c9 being Element of AFV st Mid a,b,c & Mid a,b9,c9 & MDist b,b9 holds
c = c9
let a, b, c, b9, c9 be Element of AFV; ::_thesis: ( Mid a,b,c & Mid a,b9,c9 & MDist b,b9 implies c = c9 )
assume that
A1: Mid a,b,c and
A2: Mid a,b9,c9 and
A3: MDist b,b9 ; ::_thesis: c = c9
 Mid a,b9,c by A1, A3, Th23;
hence  c = c9 by A2, Th22; ::_thesis: verum
end;

theorem Th25: :: AFVECT0:25
for AFV being WeakAffVect
for a, p, a9, b, b9 being Element of AFV st Mid a,p,a9 & Mid b,p,b9 holds
a,b // b9,a9
proof
let AFV be WeakAffVect; ::_thesis: for a, p, a9, b, b9 being Element of AFV st Mid a,p,a9 & Mid b,p,b9 holds
a,b // b9,a9
let a, p, a9, b, b9 be Element of AFV; ::_thesis: ( Mid a,p,a9 & Mid b,p,b9 implies a,b // b9,a9 )
assume that
A1: Mid a,p,a9 and
A2: Mid b,p,b9 ; ::_thesis: a,b // b9,a9
consider d being Element of AFV such that
A3: b9,p // a9,d by Def1;
 a,p // p,a9 by A1, Def3;
then A4: p,a // a9,p by Th7;
 b,p // p,b9 by A2, Def3;
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  a,b // b9,a9 by A6, Def1; ::_thesis: verum
end;

theorem :: AFVECT0:26
for AFV being WeakAffVect
for a, p, a9, b, q, b9 being Element of AFV st Mid a,p,a9 & Mid b,q,b9 & MDist p,q holds
a,b // b9,a9
proof
let AFV be WeakAffVect; ::_thesis: for a, p, a9, b, q, b9 being Element of AFV st Mid a,p,a9 & Mid b,q,b9 & MDist p,q holds
a,b // b9,a9
let a, p, a9, b, q, b9 be Element of AFV; ::_thesis: ( Mid a,p,a9 & Mid b,q,b9 & MDist p,q implies a,b // b9,a9 )
assume that
A1: Mid a,p,a9 and
A2: Mid b,q,b9 and
A3: MDist p,q ; ::_thesis: a,b // b9,a9
 Mid a,q,a9 by A1, A3, Th23;
hence  a,b // b9,a9 by A2, Th25; ::_thesis: verum
end;

definition
let AFV be WeakAffVect;
let a, b be Element of AFV;
func PSym (a,b) ->  Element of AFV means :Def4: :: AFVECT0:def 4
 Mid b,a,it;
correctness
existence
ex b1 being Element of AFV st Mid b,a,b1;
uniqueness
for b1, b2 being Element of AFV st Mid b,a,b1 & Mid b,a,b2 holds
b1 = b2;
by Th21, Th22;
end;

:: deftheorem Def4 defines PSym AFVECT0:def_4_:_
 for AFV being WeakAffVect
for a, b, b4 being Element of AFV holds
( b4 = PSym (a,b) iff Mid b,a,b4 );

theorem :: AFVECT0:27
for AFV being WeakAffVect
for p, a, b being Element of AFV holds
( PSym (p,a) = b iff a,p // p,b )
proof
let AFV be WeakAffVect; ::_thesis: for p, a, b being Element of AFV holds
( PSym (p,a) = b iff a,p // p,b )
let p, a, b be Element of AFV; ::_thesis: ( PSym (p,a) = b iff a,p // p,b )
A1: now__::_thesis:_(_a,p_//_p,b_implies_PSym_(p,a)_=_b_)
assume  a,p // p,b ; ::_thesis: PSym (p,a) = b
then  Mid a,p,b by Def3;
hence  PSym (p,a) = b by Def4; ::_thesis: verum
end;
now__::_thesis:_(_PSym_(p,a)_=_b_implies_a,p_//_p,b_)
assume  PSym (p,a) = b ; ::_thesis: a,p // p,b
then  Mid a,p,b by Def4;
hence  a,p // p,b by Def3; ::_thesis: verum
end;
hence  ( PSym (p,a) = b iff a,p // p,b ) by A1; ::_thesis: verum
end;

theorem Th28: :: AFVECT0:28
for AFV being WeakAffVect
for p, a being Element of AFV holds
( PSym (p,a) = a iff ( a = p or MDist a,p ) )
proof
let AFV be WeakAffVect; ::_thesis: for p, a being Element of AFV holds
( PSym (p,a) = a iff ( a = p or MDist a,p ) )
let p, a be Element of AFV; ::_thesis: ( PSym (p,a) = a iff ( a = p or MDist a,p ) )
A1: now__::_thesis:_(_(_a_=_p_or_MDist_a,p_)_implies_PSym_(p,a)_=_a_)
assume  ( a = p or MDist a,p ) ; ::_thesis: PSym (p,a) = a
then  Mid a,p,a by Th18;
hence  PSym (p,a) = a by Def4; ::_thesis: verum
end;
now__::_thesis:_(_not_PSym_(p,a)_=_a_or_a_=_p_or_MDist_a,p_)
assume  PSym (p,a) = a ; ::_thesis: ( a = p or MDist a,p )
then  Mid a,p,a by Def4;
hence  ( a = p or MDist a,p ) by Th18; ::_thesis: verum
end;
hence  ( PSym (p,a) = a iff ( a = p or MDist a,p ) ) by A1; ::_thesis: verum
end;

theorem Th29: :: AFVECT0:29
for AFV being WeakAffVect
for p, a being Element of AFV holds PSym (p,(PSym (p,a))) = a
proof
let AFV be WeakAffVect; ::_thesis: for p, a being Element of AFV holds PSym (p,(PSym (p,a))) = a
let p, a be Element of AFV; ::_thesis: PSym (p,(PSym (p,a))) = a
 Mid a,p, PSym (p,a) by Def4;
then  Mid PSym (p,a),p,a by Th16;
hence  PSym (p,(PSym (p,a))) = a by Def4; ::_thesis: verum
end;

theorem Th30: :: AFVECT0:30
for AFV being WeakAffVect
for p, a, b being Element of AFV st PSym (p,a) = PSym (p,b) holds
a = b
proof
let AFV be WeakAffVect; ::_thesis: for p, a, b being Element of AFV st PSym (p,a) = PSym (p,b) holds
a = b
let p, a, b be Element of AFV; ::_thesis: ( PSym (p,a) = PSym (p,b) implies a = b )
assume A1: PSym (p,a) = PSym (p,b) ; ::_thesis: a = b
 PSym (p,(PSym (p,a))) = a by Th29;
hence  a = b by A1, Th29; ::_thesis: verum
end;

theorem :: AFVECT0:31
for AFV being WeakAffVect
for p, b being Element of AFV ex a being Element of AFV st PSym (p,a) = b
proof
let AFV be WeakAffVect; ::_thesis: for p, b being Element of AFV ex a being Element of AFV st PSym (p,a) = b
let p, b be Element of AFV; ::_thesis: ex a being Element of AFV st PSym (p,a) = b
 PSym (p,(PSym (p,b))) = b by Th29;
hence  ex a being Element of AFV st PSym (p,a) = b ; ::_thesis: verum
end;

theorem Th32: :: AFVECT0:32
for AFV being WeakAffVect
for a, b, p being Element of AFV holds a,b // PSym (p,b), PSym (p,a)
proof
let AFV be WeakAffVect; ::_thesis: for a, b, p being Element of AFV holds a,b // PSym (p,b), PSym (p,a)
let a, b, p be Element of AFV; ::_thesis: a,b // PSym (p,b), PSym (p,a)
 ( Mid a,p, PSym (p,a) & Mid b,p, PSym (p,b) ) by Def4;
hence  a,b // PSym (p,b), PSym (p,a) by Th25; ::_thesis: verum
end;

theorem Th33: :: AFVECT0:33
for AFV being WeakAffVect
for a, b, c, d, p being Element of AFV holds
( a,b // c,d iff PSym (p,a), PSym (p,b) // PSym (p,c), PSym (p,d) )
proof
let AFV be WeakAffVect; ::_thesis: for a, b, c, d, p being Element of AFV holds
( a,b // c,d iff PSym (p,a), PSym (p,b) // PSym (p,c), PSym (p,d) )
let a, b, c, d, p be Element of AFV; ::_thesis: ( a,b // c,d iff PSym (p,a), PSym (p,b) // PSym (p,c), PSym (p,d) )
A1: now__::_thesis:_(_PSym_(p,a),_PSym_(p,b)_//_PSym_(p,c),_PSym_(p,d)_implies_a,b_//_c,d_)
assume A2: PSym (p,a), PSym (p,b) // PSym (p,c), PSym (p,d) ; ::_thesis: a,b // c,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; ::_thesis: verum
end;
now__::_thesis:_(_a,b_//_c,d_implies_PSym_(p,a),_PSym_(p,b)_//_PSym_(p,c),_PSym_(p,d)_)
A4: PSym (p,b), PSym (p,a) // a,b by Th3, Th32;
assume A5: a,b // c,d ; ::_thesis: PSym (p,a), PSym (p,b) // PSym (p,c), PSym (p,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; ::_thesis: verum
end;
hence  ( a,b // c,d iff PSym (p,a), PSym (p,b) // PSym (p,c), PSym (p,d) ) by A1; ::_thesis: verum
end;

theorem :: AFVECT0:34
for AFV being WeakAffVect
for a, b, p being Element of AFV holds
( MDist a,b iff MDist PSym (p,a), PSym (p,b) )
proof
let AFV be WeakAffVect; ::_thesis: for a, b, p being Element of AFV holds
( MDist a,b iff MDist PSym (p,a), PSym (p,b) )
let a, b, p be Element of AFV; ::_thesis: ( MDist a,b iff MDist PSym (p,a), PSym (p,b) )
A1: now__::_thesis:_(_MDist_a,b_implies_MDist_PSym_(p,a),_PSym_(p,b)_)
assume A2: MDist a,b ; ::_thesis: MDist PSym (p,a), PSym (p,b)
then  a,b // b,a by Def2;
then A3: PSym (p,a), PSym (p,b) // PSym (p,b), PSym (p,a) by Th33;
 PSym (p,a) <> PSym (p,b) by A2, Th30;
hence  MDist PSym (p,a), PSym (p,b) by A3, Def2; ::_thesis: verum
end;
now__::_thesis:_(_MDist_PSym_(p,a),_PSym_(p,b)_implies_MDist_a,b_)
assume A4: MDist PSym (p,a), PSym (p,b) ; ::_thesis: MDist a,b
then  PSym (p,a), PSym (p,b) // PSym (p,b), PSym (p,a) by Def2;
then  a,b // b,a by Th33;
hence  MDist a,b by A4, Def2; ::_thesis: verum
end;
hence  ( MDist a,b iff MDist PSym (p,a), PSym (p,b) ) by A1; ::_thesis: verum
end;

theorem Th35: :: AFVECT0:35
for AFV being WeakAffVect
for a, b, c, p being Element of AFV holds
( Mid a,b,c iff Mid PSym (p,a), PSym (p,b), PSym (p,c) )
proof
let AFV be WeakAffVect; ::_thesis: for a, b, c, p being Element of AFV holds
( Mid a,b,c iff Mid PSym (p,a), PSym (p,b), PSym (p,c) )
let a, b, c, p be Element of AFV; ::_thesis: ( Mid a,b,c iff Mid PSym (p,a), PSym (p,b), PSym (p,c) )
A1: now__::_thesis:_(_Mid_PSym_(p,a),_PSym_(p,b),_PSym_(p,c)_implies_Mid_a,b,c_)
assume  Mid PSym (p,a), PSym (p,b), PSym (p,c) ; ::_thesis: Mid a,b,c
then  PSym (p,a), PSym (p,b) // PSym (p,b), PSym (p,c) by Def3;
then  a,b // b,c by Th33;
hence  Mid a,b,c by Def3; ::_thesis: verum
end;
now__::_thesis:_(_Mid_a,b,c_implies_Mid_PSym_(p,a),_PSym_(p,b),_PSym_(p,c)_)
assume  Mid a,b,c ; ::_thesis: Mid PSym (p,a), PSym (p,b), PSym (p,c)
then  a,b // b,c by Def3;
then  PSym (p,a), PSym (p,b) // PSym (p,b), PSym (p,c) by Th33;
hence  Mid PSym (p,a), PSym (p,b), PSym (p,c) by Def3; ::_thesis: verum
end;
hence  ( Mid a,b,c iff Mid PSym (p,a), PSym (p,b), PSym (p,c) ) by A1; ::_thesis: verum
end;

theorem Th36: :: AFVECT0:36
for AFV being WeakAffVect
for p, a, q being Element of AFV holds
( PSym (p,a) = PSym (q,a) iff ( p = q or MDist p,q ) )
proof
let AFV be WeakAffVect; ::_thesis: for p, a, q being Element of AFV holds
( PSym (p,a) = PSym (q,a) iff ( p = q or MDist p,q ) )
let p, a, q be Element of AFV; ::_thesis: ( PSym (p,a) = PSym (q,a) iff ( p = q or MDist p,q ) )
A1: now__::_thesis:_(_MDist_p,q_implies_PSym_(p,a)_=_PSym_(q,a)_)
assume A2: MDist p,q ; ::_thesis: PSym (p,a) = PSym (q,a)
 ( Mid a,p, PSym (p,a) & Mid a,q, PSym (q,a) ) by Def4;
hence  PSym (p,a) = PSym (q,a) by A2, Th24; ::_thesis: verum
end;
now__::_thesis:_(_not_PSym_(p,a)_=_PSym_(q,a)_or_p_=_q_or_MDist_p,q_)
assume A3: PSym (p,a) = PSym (q,a) ; ::_thesis: ( p = q or MDist p,q )
 ( Mid a,p, PSym (p,a) & Mid a,q, PSym (q,a) ) by Def4;
hence  ( p = q or MDist p,q ) by A3, Th20; ::_thesis: verum
end;
hence  ( PSym (p,a) = PSym (q,a) iff ( p = q or MDist p,q ) ) by A1; ::_thesis: verum
end;

theorem Th37: :: AFVECT0:37
for AFV being WeakAffVect
for q, p, a being Element of AFV holds PSym (q,(PSym (p,(PSym (q,a))))) = PSym ((PSym (q,p)),a)
proof
let AFV be WeakAffVect; ::_thesis: for q, p, a being Element of AFV holds PSym (q,(PSym (p,(PSym (q,a))))) = PSym ((PSym (q,p)),a)
let q, p, a be Element of AFV; ::_thesis: PSym (q,(PSym (p,(PSym (q,a))))) = PSym ((PSym (q,p)),a)
 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  PSym (q,(PSym (p,(PSym (q,a))))) = PSym ((PSym (q,p)),a) by Th29; ::_thesis: verum
end;

theorem :: AFVECT0:38
for AFV being WeakAffVect
for p, q, a being Element of AFV holds
( PSym (p,(PSym (q,a))) = PSym (q,(PSym (p,a))) iff ( p = q or MDist p,q or MDist q, PSym (p,q) ) )
proof
let AFV be WeakAffVect; ::_thesis: for p, q, a being Element of AFV holds
( PSym (p,(PSym (q,a))) = PSym (q,(PSym (p,a))) iff ( p = q or MDist p,q or MDist q, PSym (p,q) ) )
let p, q, a be Element of AFV; ::_thesis: ( PSym (p,(PSym (q,a))) = PSym (q,(PSym (p,a))) iff ( p = q or MDist p,q or MDist q, PSym (p,q) ) )
A1: now__::_thesis:_(_PSym_(p,(PSym_(q,a)))_=_PSym_(q,(PSym_(p,a)))_implies_(_(_p_=_q_or_MDist_q,p_or_MDist_q,_PSym_(p,q)_)_&_(_p_=_q_or_MDist_p,q_or_MDist_q,_PSym_(p,q)_)_)_)
assume  PSym (p,(PSym (q,a))) = PSym (q,(PSym (p,a))) ; ::_thesis: ( ( p = q or MDist q,p or MDist q, PSym (p,q) ) & ( p = q or MDist p,q or MDist q, PSym (p,q) ) )
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) ) by Th18; ::_thesis: ( p = q or MDist p,q or MDist q, PSym (p,q) )
thus  ( p = q or MDist p,q or MDist q, PSym (p,q) ) by A2, Th18; ::_thesis: verum
end;
now__::_thesis:_(_(_p_=_q_or_MDist_p,q_or_MDist_q,_PSym_(p,q)_)_implies_PSym_(p,(PSym_(q,a)))_=_PSym_(q,(PSym_(p,a)))_)
assume  ( p = q or MDist p,q or MDist q, PSym (p,q) ) ; ::_thesis: PSym (p,(PSym (q,a))) = PSym (q,(PSym (p,a)))
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; ::_thesis: verum
end;
hence  ( PSym (p,(PSym (q,a))) = PSym (q,(PSym (p,a))) iff ( p = q or MDist p,q or MDist q, PSym (p,q) ) ) by A1; ::_thesis: verum
end;

theorem Th39: :: AFVECT0:39
for AFV being WeakAffVect
for p, q, r, a being Element of AFV holds PSym (p,(PSym (q,(PSym (r,a))))) = PSym (r,(PSym (q,(PSym (p,a)))))
proof
let AFV be WeakAffVect; ::_thesis: for p, q, r, a being Element of AFV holds PSym (p,(PSym (q,(PSym (r,a))))) = PSym (r,(PSym (q,(PSym (p,a)))))
let p, q, r, a be Element of AFV; ::_thesis: PSym (p,(PSym (q,(PSym (r,a))))) = PSym (r,(PSym (q,(PSym (p,a)))))
 ( 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))) by Def3;
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  PSym (p,(PSym (q,(PSym (r,a))))) = PSym (r,(PSym (q,(PSym (p,a))))) by Th4, Th7; ::_thesis: verum
end;

theorem :: AFVECT0:40
for AFV being WeakAffVect
for a, b, c, p being Element of AFV ex d being Element of AFV st PSym (a,(PSym (b,(PSym (c,p))))) = PSym (d,p)
proof
let AFV be WeakAffVect; ::_thesis: for a, b, c, p being Element of AFV ex d being Element of AFV st PSym (a,(PSym (b,(PSym (c,p))))) = PSym (d,p)
let a, b, c, p be Element of AFV; ::_thesis: ex d being Element of AFV st PSym (a,(PSym (b,(PSym (c,p))))) = PSym (d,p)
consider e being Element of AFV such that
A1: Mid a,e,c by Th19;
consider d being Element of AFV 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  ex d being Element of AFV st PSym (a,(PSym (b,(PSym (c,p))))) = PSym (d,p) by Th39; ::_thesis: verum
end;

theorem :: AFVECT0:41
for AFV being WeakAffVect
for a, p, b being Element of AFV ex c being Element of AFV st PSym (a,(PSym (c,p))) = PSym (c,(PSym (b,p)))
proof
let AFV be WeakAffVect; ::_thesis: for a, p, b being Element of AFV ex c being Element of AFV st PSym (a,(PSym (c,p))) = PSym (c,(PSym (b,p)))
let a, p, b be Element of AFV; ::_thesis: ex c being Element of AFV st PSym (a,(PSym (c,p))) = PSym (c,(PSym (b,p)))
consider c being Element of AFV 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  ex c being Element of AFV st PSym (a,(PSym (c,p))) = PSym (c,(PSym (b,p))) ; ::_thesis: verum
end;

definition
let AFV be WeakAffVect;
let o, a, b be Element of AFV;
func Padd (o,a,b) ->  Element of AFV means :Def5: :: AFVECT0:def 5
o,a // b,it;
correctness
existence
ex b1 being Element of AFV st o,a // b,b1;
uniqueness
for b1, b2 being Element of AFV st o,a // b,b1 & o,a // b,b2 holds
b1 = b2;
by Def1, Th5;
end;

:: deftheorem Def5 defines Padd AFVECT0:def_5_:_
 for AFV being WeakAffVect
for o, a, b, b5 being Element of AFV holds
( b5 = Padd (o,a,b) iff o,a // b,b5 );

notation
let AFV be WeakAffVect;
let o, a be Element of AFV;
synonym  Pcom (o,a) for  PSym (o,a);
end;

Lm1:  for AFV being WeakAffVect
for o, a, b being Element of AFV holds
( Pcom (o,a) = b iff a,o // o,b )
proof
let AFV be WeakAffVect; ::_thesis: for o, a, b being Element of AFV holds
( Pcom (o,a) = b iff a,o // o,b )
let o, a, b be Element of AFV; ::_thesis: ( Pcom (o,a) = b iff a,o // o,b )
A1: now__::_thesis:_(_a,o_//_o,b_implies_Pcom_(o,a)_=_b_)
assume  a,o // o,b ; ::_thesis: Pcom (o,a) = b
then  Mid a,o,b by Def3;
hence  Pcom (o,a) = b by Def4; ::_thesis: verum
end;
now__::_thesis:_(_Pcom_(o,a)_=_b_implies_a,o_//_o,b_)
assume  Pcom (o,a) = b ; ::_thesis: a,o // o,b
then  Mid a,o,b by Def4;
hence  a,o // o,b by Def3; ::_thesis: verum
end;
hence  ( Pcom (o,a) = b iff a,o // o,b ) by A1; ::_thesis: verum
end;

definition
let AFV be WeakAffVect;
let o be Element of AFV;
func Padd o ->  BinOp of the carrier of AFV means :Def6: :: AFVECT0:def 6
 for a, b being Element of AFV holds it . (a,b) = Padd (o,a,b);
existence
 ex b1 being BinOp of the carrier of AFV st
for a, b being Element of AFV holds b1 . (a,b) = Padd (o,a,b)
proof
deffunc H1( Element of AFV, 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 being Element of AFV holds O . (a,b) = H1(a,b) from BINOP_1:sch_4();
take  O ; ::_thesis: for a, b being Element of AFV holds O . (a,b) = Padd (o,a,b)
thus  for a, b being Element of AFV holds O . (a,b) = Padd (o,a,b) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being BinOp of the carrier of AFV st ( for a, b being Element of AFV holds b1 . (a,b) = Padd (o,a,b) ) & ( for a, b being Element of AFV holds b2 . (a,b) = Padd (o,a,b) ) holds
b1 = b2
proof
set X = the carrier of AFV;
let o1, o2 be BinOp of the carrier of AFV; ::_thesis: ( ( for a, b being Element of AFV holds o1 . (a,b) = Padd (o,a,b) ) & ( for a, b being Element of AFV holds o2 . (a,b) = Padd (o,a,b) ) implies o1 = o2 )
assume that
A2: for a, b being Element of AFV holds o1 . (a,b) = Padd (o,a,b) and
A3: for a, b being Element of AFV holds o2 . (a,b) = Padd (o,a,b) ; ::_thesis: o1 = o2
 for x being Element of [: the carrier of AFV, the carrier of AFV:] holds o1 . x = o2 . x
proof
let x be Element of [: the carrier of AFV, the carrier of AFV:]; ::_thesis: o1 . x = o2 . x
consider x1, x2 being Element of the carrier of AFV 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  o1 . x = o2 . x ; ::_thesis: verum
end;
hence  o1 = o2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines Padd AFVECT0:def_6_:_
 for AFV being WeakAffVect
for o being Element of AFV
for b3 being BinOp of the carrier of AFV holds
( b3 = Padd o iff for a, b being Element of AFV holds b3 . (a,b) = Padd (o,a,b) );

definition
let AFV be WeakAffVect;
let o be Element of AFV;
func Pcom o ->  UnOp of the carrier of AFV means :Def7: :: AFVECT0:def 7
 for a being Element of AFV holds it . a = Pcom (o,a);
existence
 ex b1 being UnOp of the carrier of AFV st
for a being Element of AFV holds b1 . a = Pcom (o,a)
proof
deffunc H1( Element of AFV) ->  Element of AFV = Pcom (o,$1);
consider O being UnOp of the carrier of AFV such that
A1: for a being Element of AFV holds O . a = H1(a) from FUNCT_2:sch_4();
take  O ; ::_thesis: for a being Element of AFV holds O . a = Pcom (o,a)
thus  for a being Element of AFV holds O . a = Pcom (o,a) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being UnOp of the carrier of AFV st ( for a being Element of AFV holds b1 . a = Pcom (o,a) ) & ( for a being Element of AFV holds b2 . a = Pcom (o,a) ) holds
b1 = b2
proof
set X = the carrier of AFV;
let o1, o2 be UnOp of the carrier of AFV; ::_thesis: ( ( for a being Element of AFV holds o1 . a = Pcom (o,a) ) & ( for a being Element of AFV holds o2 . a = Pcom (o,a) ) implies o1 = o2 )
assume that
A2: for a being Element of AFV holds o1 . a = Pcom (o,a) and
A3: for a being Element of AFV holds o2 . a = Pcom (o,a) ; ::_thesis: o1 = o2
 for x being Element of the carrier of AFV holds o1 . x = o2 . x
proof
let x be Element of the carrier of AFV; ::_thesis: o1 . x = o2 . x
o1 . x = Pcom (o,x) by A2
.= o2 . x by A3 ;
hence  o1 . x = o2 . x ; ::_thesis: verum
end;
hence  o1 = o2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines Pcom AFVECT0:def_7_:_
 for AFV being WeakAffVect
for o being Element of AFV
for b3 being UnOp of the carrier of AFV holds
( b3 = Pcom o iff for a being Element of AFV holds b3 . a = Pcom (o,a) );

definition
let AFV be WeakAffVect;
let o be Element of AFV;
func GroupVect (AFV,o) ->  strict addLoopStr  equals :: AFVECT0:def 8
 addLoopStr(# the carrier of AFV,(Padd o),o #);
correctness
coherence
addLoopStr(# the carrier of AFV,(Padd o),o #) is strict addLoopStr ;
;
end;

:: deftheorem  defines GroupVect AFVECT0:def_8_:_
 for AFV being WeakAffVect
for o being Element of AFV holds GroupVect (AFV,o) = addLoopStr(# the carrier of AFV,(Padd o),o #);

registration
let AFV be WeakAffVect;
let o be Element of AFV;
cluster GroupVect (AFV,o) ->  non empty strict ;
coherence
 not GroupVect (AFV,o) is empty ;
end;

theorem :: AFVECT0:42
for AFV being WeakAffVect
for o being Element of AFV holds
( the carrier of (GroupVect (AFV,o)) = the carrier of AFV & the addF of (GroupVect (AFV,o)) = Padd o & 0. (GroupVect (AFV,o)) = o ) ;


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

Lm2:  for AFV being WeakAffVect
for o being Element of AFV
for a, b being Element of (GroupVect (AFV,o)) holds a + b = b + a
proof
let AFV be WeakAffVect; ::_thesis: for o being Element of AFV
for a, b being Element of (GroupVect (AFV,o)) holds a + b = b + a
let o be Element of AFV; ::_thesis: for a, b being Element of (GroupVect (AFV,o)) holds a + b = b + a
let a, b be Element of (GroupVect (AFV,o)); ::_thesis: a + b = b + a
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  a + b = b + a ; ::_thesis: verum
end;

Lm3:  for AFV being WeakAffVect
for o being Element of AFV
for a, b, c being Element of (GroupVect (AFV,o)) holds (a + b) + c = a + (b + c)
proof
let AFV be WeakAffVect; ::_thesis: for o being Element of AFV
for a, b, c being Element of (GroupVect (AFV,o)) holds (a + b) + c = a + (b + c)
let o be Element of AFV; ::_thesis: for a, b, c being Element of (GroupVect (AFV,o)) holds (a + b) + c = a + (b + c)
let a, b, c be Element of (GroupVect (AFV,o)); ::_thesis: (a + b) + c = a + (b + c)
reconsider a9 = a, b9 = b, c9 = c as Element of AFV ;
set p = b + c;
set q = a + b;
reconsider p9 = b + c, q9 = a + b as Element of AFV ;
reconsider x9 = a + (b + c), y9 = (a + b) + c as Element of AFV ;
consider x99 being Element of AFV 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  (a + b) + c = a + (b + c) by Th4; ::_thesis: verum
end;

Lm4:  for AFV being WeakAffVect
for o being Element of AFV
for a being Element of (GroupVect (AFV,o)) holds a + (0. (GroupVect (AFV,o))) = a
proof
let AFV be WeakAffVect; ::_thesis: for o being Element of AFV
for a being Element of (GroupVect (AFV,o)) holds a + (0. (GroupVect (AFV,o))) = a
let o be Element of AFV; ::_thesis: for a being Element of (GroupVect (AFV,o)) holds a + (0. (GroupVect (AFV,o))) = a
let a be Element of (GroupVect (AFV,o)); ::_thesis: a + (0. (GroupVect (AFV,o))) = a
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  a + (0. (GroupVect (AFV,o))) = a by Th4; ::_thesis: verum
end;

Lm5:  for AFV being WeakAffVect
for o being Element of AFV holds
( GroupVect (AFV,o) is Abelian & GroupVect (AFV,o) is add-associative & GroupVect (AFV,o) is right_zeroed )
proof
let AFV be WeakAffVect; ::_thesis: for o being Element of AFV holds
( GroupVect (AFV,o) is Abelian & GroupVect (AFV,o) is add-associative & GroupVect (AFV,o) is right_zeroed )
let o be Element of AFV; ::_thesis: ( GroupVect (AFV,o) is Abelian & GroupVect (AFV,o) is add-associative & GroupVect (AFV,o) is right_zeroed )
thus  for a, b being Element of (GroupVect (AFV,o)) holds a + b = b + a by Lm2; :: according to RLVECT_1:def_2 ::_thesis: ( GroupVect (AFV,o) is add-associative & GroupVect (AFV,o) is right_zeroed )
thus  for a, b, c being Element of (GroupVect (AFV,o)) holds (a + b) + c = a + (b + c) by Lm3; :: according to RLVECT_1:def_3 ::_thesis: GroupVect (AFV,o) is right_zeroed
thus  for a being Element of (GroupVect (AFV,o)) holds a + (0. (GroupVect (AFV,o))) = a by Lm4; :: according to RLVECT_1:def_4 ::_thesis: verum
end;

Lm6:  for AFV being WeakAffVect
for o being Element of AFV holds GroupVect (AFV,o) is right_complementable
proof
let AFV be WeakAffVect; ::_thesis: for o being Element of AFV holds GroupVect (AFV,o) is right_complementable
let o be Element of AFV; ::_thesis: GroupVect (AFV,o) is right_complementable
let s be Element of (GroupVect (AFV,o)); :: according to ALGSTR_0:def_16 ::_thesis: s is right_complementable
reconsider s9 = s as Element of AFV ;
reconsider t = (Pcom o) . s9 as Element of (GroupVect (AFV,o)) ;
take  t ; :: according to ALGSTR_0:def_11 ::_thesis: s + t = 0. (GroupVect (AFV,o))
 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 ; ::_thesis: verum
end;

registration
let AFV be WeakAffVect;
let o be Element of AFV;
cluster GroupVect (AFV,o) ->  strict right_complementable Abelian add-associative right_zeroed ;
coherence
 ( GroupVect (AFV,o) is Abelian & GroupVect (AFV,o) is add-associative & GroupVect (AFV,o) is right_zeroed & GroupVect (AFV,o) is right_complementable ) by Lm5, Lm6;
end;

theorem Th44: :: AFVECT0:44
for AFV being WeakAffVect
for o being Element of AFV
for a being Element of (GroupVect (AFV,o))
for a9 being Element of AFV st a = a9 holds
- a = (Pcom o) . a9
proof
let AFV be WeakAffVect; ::_thesis: for o being Element of AFV
for a being Element of (GroupVect (AFV,o))
for a9 being Element of AFV st a = a9 holds
- a = (Pcom o) . a9
let o be Element of AFV; ::_thesis: for a being Element of (GroupVect (AFV,o))
for a9 being Element of AFV st a = a9 holds
- a = (Pcom o) . a9
let a be Element of (GroupVect (AFV,o)); ::_thesis: for a9 being Element of AFV st a = a9 holds
- a = (Pcom o) . a9
let a9 be Element of AFV; ::_thesis: ( a = a9 implies - a = (Pcom o) . a9 )
assume A1: a = a9 ; ::_thesis: - a = (Pcom o) . 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  - a = (Pcom o) . a9 by RLVECT_1:def_10; ::_thesis: verum
end;

theorem :: AFVECT0:45
for AFV being WeakAffVect
for o being Element of AFV holds 0. (GroupVect (AFV,o)) = o ;


theorem Th46: :: AFVECT0:46
for AFV being WeakAffVect
for o being Element of AFV
for a being Element of (GroupVect (AFV,o)) ex b being Element of (GroupVect (AFV,o)) st b + b = a
proof
let AFV be WeakAffVect; ::_thesis: for o being Element of AFV
for a being Element of (GroupVect (AFV,o)) ex b being Element of (GroupVect (AFV,o)) st b + b = a
let o be Element of AFV; ::_thesis: for a being Element of (GroupVect (AFV,o)) ex b being Element of (GroupVect (AFV,o)) st b + b = a
let a be Element of (GroupVect (AFV,o)); ::_thesis: ex b being Element of (GroupVect (AFV,o)) st b + b = 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  ex b being Element of (GroupVect (AFV,o)) st b + b = a ; ::_thesis: verum
end;

registration
let AFV be WeakAffVect;
let o be Element of AFV;
cluster GroupVect (AFV,o) ->  strict Two_Divisible ;
coherence
 GroupVect (AFV,o) is Two_Divisible
proof
 for a being Element of (GroupVect (AFV,o)) ex b being Element of (GroupVect (AFV,o)) st b + b = a by Th46;
hence  GroupVect (AFV,o) is Two_Divisible by TDGROUP:def_1; ::_thesis: verum
end;
end;


theorem Th47: :: AFVECT0:47
for AFV being AffVect
for o being Element of AFV
for a being Element of (GroupVect (AFV,o)) st a + a = 0. (GroupVect (AFV,o)) holds
a = 0. (GroupVect (AFV,o))
proof
let AFV be AffVect; ::_thesis: for o being Element of AFV
for a being Element of (GroupVect (AFV,o)) st a + a = 0. (GroupVect (AFV,o)) holds
a = 0. (GroupVect (AFV,o))
let o be Element of AFV; ::_thesis: for a being Element of (GroupVect (AFV,o)) st a + a = 0. (GroupVect (AFV,o)) holds
a = 0. (GroupVect (AFV,o))
let a be Element of (GroupVect (AFV,o)); ::_thesis: ( a + a = 0. (GroupVect (AFV,o)) implies a = 0. (GroupVect (AFV,o)) )
assume A1: a + a = 0. (GroupVect (AFV,o)) ; ::_thesis: 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  a = 0. (GroupVect (AFV,o)) by A2, TDGROUP:16; ::_thesis: verum
end;

registration
let AFV be AffVect;
let o be Element of AFV;
cluster GroupVect (AFV,o) ->  strict Fanoian ;
coherence
 GroupVect (AFV,o) is Fanoian
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  GroupVect (AFV,o) is Fanoian by VECTSP_1:def_18; ::_thesis: verum
end;
end;

registration
cluster non empty non trivial strict right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible for addLoopStr ;
existence
 ex b1 being Uniquely_Two_Divisible_Group st
( b1 is strict & not b1 is trivial )
proof
set X = G_Real ;
 not G_Real is trivial by STRUCT_0:def_10, TDGROUP:6;
hence  ex b1 being Uniquely_Two_Divisible_Group st
( b1 is strict & not b1 is trivial ) ; ::_thesis: verum
end;
end;

definition
mode Proper_Uniquely_Two_Divisible_Group is non trivial Uniquely_Two_Divisible_Group;
end;

theorem :: AFVECT0:48
for AFV being AffVect
for o being Element of AFV holds GroupVect (AFV,o) is Proper_Uniquely_Two_Divisible_Group ;

registration
let AFV be AffVect;
let o be Element of AFV;
cluster GroupVect (AFV,o) ->  non trivial strict ;
coherence
 not GroupVect (AFV,o) is trivial ;
end;

theorem Th49: :: AFVECT0:49
for ADG being Proper_Uniquely_Two_Divisible_Group holds AV ADG is AffVect
proof
let ADG be Proper_Uniquely_Two_Divisible_Group; ::_thesis: AV ADG is AffVect
 ex a, b being Element of ADG st a <> b by STRUCT_0:def_10;
hence  AV ADG is AffVect by TDGROUP:17; ::_thesis: verum
end;

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

theorem Th50: :: AFVECT0:50
for AFV being strict AffVect
for o being Element of AFV holds AFV = AV (GroupVect (AFV,o))
proof
let AFV be strict AffVect; ::_thesis: for o being Element of AFV holds AFV = AV (GroupVect (AFV,o))
let o be Element of AFV; ::_thesis: AFV = AV (GroupVect (AFV,o))
set X = GroupVect (AFV,o);
now__::_thesis:_for_x,_y_being_set_holds_
(_[x,y]_in_CONGRD_(GroupVect_(AFV,o))_iff_[x,y]_in_the_CONGR_of_AFV_)
let x, y be set ; ::_thesis: ( [x,y] in CONGRD (GroupVect (AFV,o)) iff [x,y] in the CONGR of AFV )
set xy = [x,y];
A1: now__::_thesis:_(_[x,y]_in_the_CONGR_of_AFV_implies_[x,y]_in_CONGRD_(GroupVect_(AFV,o))_)
set V = the carrier of AFV;
assume A2: [x,y] in the CONGR of AFV ; ::_thesis: [x,y] in CONGRD (GroupVect (AFV,o))
set VV = [: the carrier of AFV, the carrier of AFV:];
 [x,y] `2 = y ;
then A3: y in [: the carrier of AFV, the carrier of AFV:] by A2, MCART_1:10;
then A4: y = [(y `1),(y `2)] by MCART_1:21;
 [x,y] `1 = x ;
then A5: x in [: the carrier of AFV, the carrier of AFV:] 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 (GroupVect (AFV,o)) ;
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  x19 # y29 = x29 # y19 by A8, Def5; ::_thesis: verum
end;
hence  [x,y] in CONGRD (GroupVect (AFV,o)) by A6, A4, TDGROUP:def_2; ::_thesis: verum
end;
now__::_thesis:_(_[x,y]_in_CONGRD_(GroupVect_(AFV,o))_implies_[x,y]_in_the_CONGR_of_AFV_)
set V = the carrier of (GroupVect (AFV,o));
assume A9: [x,y] in CONGRD (GroupVect (AFV,o)) ; ::_thesis: [x,y] in the CONGR of AFV
set VV = [: the carrier of (GroupVect (AFV,o)), the carrier of (GroupVect (AFV,o)):];
 [x,y] `2 = y ;
then A10: y in [: the carrier of (GroupVect (AFV,o)), the carrier of (GroupVect (AFV,o)):] by A9, MCART_1:10;
then A11: y = [(y `1),(y `2)] by MCART_1:21;
 [x,y] `1 = x ;
then A12: x in [: the carrier of (GroupVect (AFV,o)), the carrier of (GroupVect (AFV,o)):] by A9, MCART_1:10;
then reconsider x19 = x `1 , x29 = x `2 , y19 = y `1 , y29 = y `2 as Element of (GroupVect (AFV,o)) by A10, MCART_1:10;
set z19 = x19 # y29;
set z29 = x29 # y19;
reconsider x1 = x19, x2 = x29, y1 = y19, y2 = y29 as Element of AFV ;
reconsider z1 = x19 # y29, z2 = x29 # y19 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  x19 # y29 = x29 # y19 by A9, A11, TDGROUP:def_2;
then  o,x2 // y1,z1 by A13, Def5;
then  x1,x2 // y1,y2 by A14, Th12;
hence  [x,y] in the CONGR of AFV by A15, A11, ANALOAF:def_2; ::_thesis: verum
end;
hence  ( [x,y] in CONGRD (GroupVect (AFV,o)) iff [x,y] in the CONGR of AFV ) by A1; ::_thesis: verum
end;
then  ( the carrier of (AV (GroupVect (AFV,o))) = the carrier of AFV & CONGRD (GroupVect (AFV,o)) = the CONGR of AFV ) by RELAT_1:def_2, TDGROUP:4;
hence  AFV = AV (GroupVect (AFV,o)) by TDGROUP:4; ::_thesis: verum
end;

theorem :: AFVECT0:51
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 ; ::_thesis: ( AS is AffVect iff ex ADG being Proper_Uniquely_Two_Divisible_Group st AS = AV ADG )
now__::_thesis:_(_AS_is_AffVect_implies_ex_ADG_being_strict_addLoopStr_ex_ADG_being_Proper_Uniquely_Two_Divisible_Group_st_AS_=_AV_ADG_)
assume  AS is AffVect ; ::_thesis: ex ADG being strict addLoopStr ex ADG being Proper_Uniquely_Two_Divisible_Group st AS = AV ADG
then reconsider AS9 = AS as AffVect ;
set o = the Element of AS9;
take ADG = GroupVect (AS9, the Element of AS9); ::_thesis: ex ADG being Proper_Uniquely_Two_Divisible_Group st AS = AV ADG
 AS9 = AV ADG by Th50;
hence  ex ADG being Proper_Uniquely_Two_Divisible_Group st AS = AV ADG ; ::_thesis: verum
end;
hence  ( AS is AffVect iff ex ADG being Proper_Uniquely_Two_Divisible_Group st AS = AV ADG ) ; ::_thesis: verum
end;

definition
let X, Y be non empty addLoopStr ;
let f be Function of the carrier of X, the carrier of Y;
predf is_Iso_of X,Y means :Def9: :: AFVECT0:def 9
( 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;

:: deftheorem Def9 defines is_Iso_of AFVECT0:def_9_:_
 for X, Y being non empty addLoopStr
for f being Function of the carrier of X, the carrier of Y holds
( f is_Iso_of X,Y iff ( 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) ) ) ) );

definition
let X, Y be non empty addLoopStr ;
predX,Y are_Iso  means :Def10: :: AFVECT0:def 10
 ex f being Function of the carrier of X, the carrier of Y st f is_Iso_of X,Y;
end;

:: deftheorem Def10 defines are_Iso AFVECT0:def_10_:_
 for X, Y being non empty addLoopStr holds
( X,Y are_Iso iff ex f being Function of the carrier of X, the carrier of Y st f is_Iso_of X,Y );


theorem Th52: :: AFVECT0:52
for ADG being Proper_Uniquely_Two_Divisible_Group
for f being Function of the carrier of ADG, the carrier of ADG
for o9 being Element of ADG
for 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 ADG be Proper_Uniquely_Two_Divisible_Group; ::_thesis: for f being Function of the carrier of ADG, the carrier of ADG
for o9 being Element of ADG
for 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) )
let f be Function of the carrier of ADG, the carrier of ADG; ::_thesis: for o9 being Element of ADG
for 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) )
let o9 be Element of ADG; ::_thesis: for 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) )
let o be Element of (AV ADG); ::_thesis: ( ( for x being Element of ADG holds f . x = o9 + x ) & o = o9 implies 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) ) )
assume that
A1: for x being Element of ADG holds f . x = o9 + x and
A2: o = o9 ; ::_thesis: 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) )
let a, b be Element of ADG; ::_thesis: ( f . (a + b) = (Padd o) . ((f . a),(f . b)) & f . (0. ADG) = 0. (GroupVect ((AV ADG),o)) & f . (- a) = (Pcom o) . (f . a) )
set a9 = f . a;
set b9 = f . b;
A3: AV ADG = AffinStruct(# the carrier of ADG,(CONGRD ADG) #) by TDGROUP:def_3;
then reconsider a99 = f . a, b99 = f . b as Element of (AV ADG) ;
thus  f . (a + b) = (Padd o) . ((f . a),(f . b)) ::_thesis: ( f . (0. ADG) = 0. (GroupVect ((AV ADG),o)) & f . (- a) = (Pcom o) . (f . a) )
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,(f . a)],[(f . b),c9]] in CONGRD ADG by A2, A3, ANALOAF:def_2;
then A5: o9 + c9 = (f . a) + (f . b) by TDGROUP:def_2;
 ( f . a = o9 + a & f . b = 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  f . (a + b) = (Padd o) . ((f . a),(f . b)) ; ::_thesis: verum
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)) ; ::_thesis: f . (- a) = (Pcom o) . (f . a)
thus  f . (- a) = (Pcom o) . (f . a) ::_thesis: verum
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  [[(f . a),o9],[o9,c9]] in CONGRD ADG by A2, A3, ANALOAF:def_2;
then  (f . a) + 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  f . (- a) = (Pcom o) . (f . a) ; ::_thesis: verum
end;
end;

theorem Th53: :: AFVECT0:53
for ADG being Proper_Uniquely_Two_Divisible_Group
for f being Function of the carrier of ADG, the carrier of ADG
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 ADG be Proper_Uniquely_Two_Divisible_Group; ::_thesis: for f being Function of the carrier of ADG, the carrier of ADG
for o9 being Element of ADG st ( for b being Element of ADG holds f . b = o9 + b ) holds
f is one-to-one
let f be Function of the carrier of ADG, the carrier of ADG; ::_thesis: for o9 being Element of ADG st ( for b being Element of ADG holds f . b = o9 + b ) holds
f is one-to-one
let o9 be Element of ADG; ::_thesis: ( ( for b being Element of ADG holds f . b = o9 + b ) implies f is one-to-one )
assume A1: for b being Element of ADG holds f . b = o9 + b ; ::_thesis: f is one-to-one
now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_f_&_x2_in_dom_f_&_f_._x1_=_f_._x2_holds_
x1_=_x2
let x1, x2 be set ; ::_thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A2: ( x1 in dom f & x2 in dom f ) and
A3: f . x1 = f . x2 ; ::_thesis: x1 = 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; ::_thesis: verum
end;
hence  f is one-to-one by FUNCT_1:def_4; ::_thesis: verum
end;

theorem Th54: :: AFVECT0:54
for ADG being Proper_Uniquely_Two_Divisible_Group
for f being Function of the carrier of ADG, the carrier of ADG
for o9 being Element of ADG
for 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
let ADG be Proper_Uniquely_Two_Divisible_Group; ::_thesis: for f being Function of the carrier of ADG, the carrier of ADG
for o9 being Element of ADG
for 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))
let f be Function of the carrier of ADG, the carrier of ADG; ::_thesis: for o9 being Element of ADG
for 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))
set X = the carrier of ADG;
A1: the carrier of ADG = dom f by FUNCT_2:def_1;
let o9 be Element of ADG; ::_thesis: for 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))
let o be Element of (AV ADG); ::_thesis: ( ( for b being Element of ADG holds f . b = o9 + b ) implies rng f = the carrier of (GroupVect ((AV ADG),o)) )
assume A2: for b being Element of ADG holds f . b = o9 + b ; ::_thesis: rng f = the carrier of (GroupVect ((AV ADG),o))
now__::_thesis:_for_y_being_set_st_y_in_the_carrier_of_ADG_holds_
y_in_rng_f
let y be set ; ::_thesis: ( y in the carrier of ADG implies y in rng f )
assume  y in the carrier of ADG ; ::_thesis: y in rng f
then reconsider y9 = y as Element of the carrier of ADG ;
set x9 = y9 - o9;
f . (y9 - o9) = 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; ::_thesis: verum
end;
then A3: the carrier of ADG c= rng f by TARSKI:def_3;
 ( rng f c= the carrier of ADG & the carrier of ADG = the carrier of (GroupVect ((AV ADG),o)) ) by RELAT_1:def_19, TDGROUP:4;
hence  rng f = the carrier of (GroupVect ((AV ADG),o)) by A3, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: AFVECT0:55
for ADG being Proper_Uniquely_Two_Divisible_Group
for o9 being Element of ADG
for 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; ::_thesis: for o9 being Element of ADG
for o being Element of (AV ADG) st o = o9 holds
ADG, GroupVect ((AV ADG),o) are_Iso
let o9 be Element of ADG; ::_thesis: for o being Element of (AV ADG) st o = o9 holds
ADG, GroupVect ((AV ADG),o) are_Iso
let o be Element of (AV ADG); ::_thesis: ( o = o9 implies ADG, GroupVect ((AV ADG),o) are_Iso )
assume A1: o = o9 ; ::_thesis: ADG, GroupVect ((AV ADG),o) are_Iso
set AS = AV ADG;
set X = the carrier of ADG;
set Z = GroupVect ((AV ADG),o);
set T = the carrier of (GroupVect ((AV ADG),o));
deffunc H1( Element of the carrier of ADG) ->  Element of the carrier of ADG = o9 + $1;
consider g being UnOp of the carrier of ADG such that
A2: for a being Element of the carrier of ADG holds g . a = H1(a) from FUNCT_2:sch_4();
 the carrier of ADG = the carrier of (GroupVect ((AV ADG),o)) by TDGROUP:4;
then reconsider f = g as Function of the carrier of ADG, the carrier of (GroupVect ((AV ADG),o)) ;
A3: now__::_thesis:_for_a,_b_being_Element_of_ADG_holds_
(_f_._(a_+_b)_=_(f_._a)_+_(f_._b)_&_f_._(0._ADG)_=_0._(GroupVect_((AV_ADG),o))_&_f_._(-_a)_=_-_(f_._a)_)
let a, b be Element of ADG; ::_thesis: ( f . (a + b) = (f . a) + (f . b) & f . (0. ADG) = 0. (GroupVect ((AV ADG),o)) & f . (- a) = - (f . a) )
reconsider fa = f . a as Element of (AV ADG) ;
thus  f . (a + b) = (f . a) + (f . b) by A1, A2, Th52; ::_thesis: ( f . (0. ADG) = 0. (GroupVect ((AV ADG),o)) & f . (- a) = - (f . a) )
thus  f . (0. ADG) = 0. (GroupVect ((AV ADG),o)) by A1, A2, Th52; ::_thesis: f . (- a) = - (f . a)
thus f . (- a) = (Pcom o) . fa by A1, A2, Th52
.= - (f . a) by Th44 ; ::_thesis: verum
end;
 ( f is one-to-one & rng f = the carrier of (GroupVect ((AV ADG),o)) ) by A2, Th53, Th54;
then  f is_Iso_of ADG, GroupVect ((AV ADG),o) by A3, Def9;
hence  ADG, GroupVect ((AV ADG),o) are_Iso by Def10; ::_thesis: verum
end;