:: by Grzegorz Lewandowski, Krzysztof Pra\.zmowski and Bo\.zena Lewandowska

::

:: Received September 24, 1990

:: Copyright (c) 1990-2021 Association of Mizar Users

definition

let IT be non empty AffinStruct ;

end;
attr IT 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 ) );

( ( 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 ) );

:: 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 ) ) );

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

existence

ex b_{1} being non trivial AffinStruct st

( b_{1} is strict & b_{1} is WeakAffVect-like )

end;
ex b

( b

proof end;

registration

coherence

for b_{1} being non empty AffinStruct st b_{1} is AffVect-like holds

b_{1} is WeakAffVect-like
by TDGROUP:def 5;

end;
for b

b

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

for a, b, c, d, d9 being Element of AFV st a,b // c,d & a,b // c,d9 holds

d = d9

proof 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

for a, b, c, d, b9 being Element of AFV st a,b // c,d & a,c // b9,d holds

b = b9

proof end;

theorem :: AFVECT0:9

for AFV being WeakAffVect

for a, b, c, d, b9, c9, d9 being Element of AFV st b,c // b9,c9 & a,d // b,c & a,d9 // b9,c9 holds

d = d9

for a, b, c, d, b9, c9, d9 being Element of AFV st b,c // b9,c9 & a,d // b,c & a,d9 // b9,c9 holds

d = d9

proof end;

theorem :: AFVECT0:10

for AFV being WeakAffVect

for a, b, c, d, a9, b9, d9 being Element of AFV st a,b // a9,b9 & c,d // b,a & c,d9 // b9,a9 holds

d = d9

for a, b, c, d, a9, b9, d9 being Element of AFV st a,b // a9,b9 & c,d // b,a & c,d9 // b9,a9 holds

d = d9

proof end;

theorem :: AFVECT0:11

for AFV being WeakAffVect

for a, b, c, d, f, a9, b9, c9, d9, 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

for a, b, c, d, f, a9, b9, c9, d9, 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 end;

theorem Th12: :: AFVECT0:12

for AFV being WeakAffVect

for a, b, c, a9, b9, c9 being Element of AFV st a,b // a9,b9 & a,c // c9,b9 holds

b,c // c9,a9

for a, b, c, a9, b9, c9 being Element of AFV st a,b // a9,b9 & a,c // c9,b9 holds

b,c // c9,a9

proof end;

::

:: Relation of Maximal Distance

::

:: Relation of Maximal Distance

::

definition

let AFV be WeakAffVect;

let a, b be Element of AFV;

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;
let a, b be Element of AFV;

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;

:: deftheorem 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 ) );

for AFV being WeakAffVect

for a, b being Element of AFV holds

( MDist a,b iff ( a,b // b,a & a <> b ) );

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

for a, b, c being Element of AFV st MDist a,b & MDist a,c & not b = c holds

MDist b,c

proof 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

for a, b, c, d being Element of AFV st MDist a,b & a,b // c,d holds

MDist c,d

proof end;

::

:: Midpoint Relation

::

:: Midpoint Relation

::

:: 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 );

for AFV being WeakAffVect

for a, b, c being Element of AFV holds

( Mid a,b,c iff a,b // b,c );

theorem :: AFVECT0:17

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

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 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

for a, b, c, c9 being Element of AFV st Mid a,b,c & Mid a,b,c9 holds

c = c9

proof 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

for a, b, c, b9 being Element of AFV st Mid a,b,c & MDist b,b9 holds

Mid a,b9,c

proof 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

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 end;

theorem Th25: :: AFVECT0:25

for AFV being WeakAffVect

for a, b, a9, b9, p being Element of AFV st Mid a,p,a9 & Mid b,p,b9 holds

a,b // b9,a9

for a, b, a9, b9, p being Element of AFV st Mid a,p,a9 & Mid b,p,b9 holds

a,b // b9,a9

proof end;

theorem :: AFVECT0:26

for AFV being WeakAffVect

for a, b, a9, b9, p, q being Element of AFV st Mid a,p,a9 & Mid b,q,b9 & MDist p,q holds

a,b // b9,a9

for a, b, a9, b9, p, q being Element of AFV st Mid a,p,a9 & Mid b,q,b9 & MDist p,q holds

a,b // b9,a9

proof end;

::

:: Point Symmetry

::

:: Point Symmetry

::

definition

let AFV be WeakAffVect;

let a, b be Element of AFV;

correctness

existence

ex b_{1} being Element of AFV st Mid b,a,b_{1};

uniqueness

for b_{1}, b_{2} being Element of AFV st Mid b,a,b_{1} & Mid b,a,b_{2} holds

b_{1} = b_{2};

by Th21, Th22;

end;
let a, b be Element of AFV;

correctness

existence

ex b

uniqueness

for b

b

by Th21, Th22;

:: deftheorem Def4 defines PSym AFVECT0:def 4 :

for AFV being WeakAffVect

for a, b, b_{4} being Element of AFV holds

( b_{4} = PSym (a,b) iff Mid b,a,b_{4} );

for AFV being WeakAffVect

for a, b, b

( b

theorem :: AFVECT0:27

theorem Th28: :: AFVECT0:28

for AFV being WeakAffVect

for a, p being Element of AFV holds

( PSym (p,a) = a iff ( a = p or MDist a,p ) )

for a, p being Element of AFV holds

( PSym (p,a) = a iff ( a = p or MDist a,p ) )

proof 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) )

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 end;

theorem :: AFVECT0:34

theorem Th36: :: AFVECT0:36

for AFV being WeakAffVect

for a, p, q being Element of AFV holds

( PSym (p,a) = PSym (q,a) iff ( p = q or MDist p,q ) )

for a, p, q being Element of AFV holds

( PSym (p,a) = PSym (q,a) iff ( p = q or MDist p,q ) )

proof end;

theorem Th37: :: AFVECT0:37

for AFV being WeakAffVect

for a, p, q being Element of AFV holds PSym (q,(PSym (p,(PSym (q,a))))) = PSym ((PSym (q,p)),a)

for a, p, q being Element of AFV holds PSym (q,(PSym (p,(PSym (q,a))))) = PSym ((PSym (q,p)),a)

proof end;

theorem :: AFVECT0:38

for AFV being WeakAffVect

for a, p, q 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) ) )

for a, p, q 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 end;

theorem Th39: :: AFVECT0:39

for AFV being WeakAffVect

for a, p, q, r being Element of AFV holds PSym (p,(PSym (q,(PSym (r,a))))) = PSym (r,(PSym (q,(PSym (p,a)))))

for a, p, q, r being Element of AFV holds PSym (p,(PSym (q,(PSym (r,a))))) = PSym (r,(PSym (q,(PSym (p,a)))))

proof 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)

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 end;

theorem :: AFVECT0:41

for AFV being WeakAffVect

for a, b, p being Element of AFV ex c being Element of AFV st PSym (a,(PSym (c,p))) = PSym (c,(PSym (b,p)))

for a, b, p being Element of AFV ex c being Element of AFV st PSym (a,(PSym (c,p))) = PSym (c,(PSym (b,p)))

proof end;

::

:: Addition on the carrier

::

:: Addition on the carrier

::

definition

let AFV be WeakAffVect;

let o, a, b be Element of AFV;

correctness

existence

ex b_{1} being Element of AFV st o,a // b,b_{1};

uniqueness

for b_{1}, b_{2} being Element of AFV st o,a // b,b_{1} & o,a // b,b_{2} holds

b_{1} = b_{2};

by Def1, Th5;

end;
let o, a, b be Element of AFV;

correctness

existence

ex b

uniqueness

for b

b

by Def1, Th5;

:: deftheorem Def5 defines Padd AFVECT0:def 5 :

for AFV being WeakAffVect

for o, a, b, b_{5} being Element of AFV holds

( b_{5} = Padd (o,a,b) iff o,a // b,b_{5} );

for AFV being WeakAffVect

for o, a, b, b

( b

Lm1: for AFV being WeakAffVect

for a, b, o being Element of AFV holds

( Pcom (o,a) = b iff a,o // o,b )

by Def4, Def3;

definition

let AFV be WeakAffVect;

let o be Element of AFV;

ex b_{1} being BinOp of the carrier of AFV st

for a, b being Element of AFV holds b_{1} . (a,b) = Padd (o,a,b)

for b_{1}, b_{2} being BinOp of the carrier of AFV st ( for a, b being Element of AFV holds b_{1} . (a,b) = Padd (o,a,b) ) & ( for a, b being Element of AFV holds b_{2} . (a,b) = Padd (o,a,b) ) holds

b_{1} = b_{2}

end;
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 for a, b being Element of AFV holds it . (a,b) = Padd (o,a,b);

ex b

for a, b being Element of AFV holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def6 defines Padd AFVECT0:def 6 :

for AFV being WeakAffVect

for o being Element of AFV

for b_{3} being BinOp of the carrier of AFV holds

( b_{3} = Padd o iff for a, b being Element of AFV holds b_{3} . (a,b) = Padd (o,a,b) );

for AFV being WeakAffVect

for o being Element of AFV

for b

( b

definition

let AFV be WeakAffVect;

let o be Element of AFV;

ex b_{1} being UnOp of the carrier of AFV st

for a being Element of AFV holds b_{1} . a = Pcom (o,a)

for b_{1}, b_{2} being UnOp of the carrier of AFV st ( for a being Element of AFV holds b_{1} . a = Pcom (o,a) ) & ( for a being Element of AFV holds b_{2} . a = Pcom (o,a) ) holds

b_{1} = b_{2}

end;
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 for a being Element of AFV holds it . a = Pcom (o,a);

ex b

for a being Element of AFV holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def7 defines Pcom AFVECT0:def 7 :

for AFV being WeakAffVect

for o being Element of AFV

for b_{3} being UnOp of the carrier of AFV holds

( b_{3} = Pcom o iff for a being Element of AFV holds b_{3} . a = Pcom (o,a) );

for AFV being WeakAffVect

for o being Element of AFV

for b

( b

definition

let AFV be WeakAffVect;

let o be Element of AFV;

coherence

addLoopStr(# the carrier of AFV,(Padd o),o #) is strict addLoopStr ;

;

end;
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 addLoopStr(# the carrier of AFV,(Padd o),o #);

coherence

addLoopStr(# the carrier of AFV,(Padd o),o #) is strict addLoopStr ;

;

:: 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 #);

for AFV being WeakAffVect

for o being Element of AFV holds GroupVect (AFV,o) = addLoopStr(# the carrier of AFV,(Padd o),o #);

registration
end;

theorem :: AFVECT0:42

theorem :: AFVECT0:43

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 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 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 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 end;

Lm6: for AFV being WeakAffVect

for o being Element of AFV holds GroupVect (AFV,o) is right_complementable

proof end;

registration

let AFV be WeakAffVect;

let o be Element of AFV;

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;
let o be Element of AFV;

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;

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

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 end;

theorem :: AFVECT0:45

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

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 end;

registration

let AFV be WeakAffVect;

let o be Element of AFV;

coherence

GroupVect (AFV,o) is Two_Divisible

end;
let o be Element of AFV;

coherence

GroupVect (AFV,o) is Two_Divisible

proof 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))

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 end;

registration
end;

registration

ex b_{1} being Uniquely_Two_Divisible_Group st

( b_{1} is strict & not b_{1} is trivial )
end;

cluster non empty non trivial strict right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible for addLoopStr ;

existence ex b

( b

proof end;

definition
end;

theorem :: AFVECT0:48

for AFV being AffVect

for o being Element of AFV holds GroupVect (AFV,o) is Proper_Uniquely_Two_Divisible_Group ;

for o being Element of AFV holds GroupVect (AFV,o) is Proper_Uniquely_Two_Divisible_Group ;

registration
end;

registration

let ADG be Proper_Uniquely_Two_Divisible_Group;

coherence

( AV ADG is AffVect-like & not AV ADG is trivial ) by Th49;

end;
coherence

( AV ADG is AffVect-like & not AV ADG is trivial ) by Th49;

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 )

( AS is AffVect iff ex ADG being Proper_Uniquely_Two_Divisible_Group st AS = AV ADG )

proof end;

definition
end;

:: deftheorem 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) ) ) ) );

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) ) ) ) );

:: deftheorem 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 );

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) )

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 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

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 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))

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 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

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 end;

:: Properties of Relation of Congruence of Vectors

::