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