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