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