let AS be strict AffinStruct ; :: thesis: ( AS is AffVect iff ex ADG being Proper_Uniquely_Two_Divisible_Group st AS = AV ADG )

now

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 ;
consider o being Element of AS9;
take ADG = GroupVect AS9,o; :: thesis: ex ADG being Proper_Uniquely_Two_Divisible_Group st AS = AV ADG
AS9 = AV ADG by Th71;
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