( dom g = Seg (len g) & Seg (len (carr g)) = dom (carr g) ) by FINSEQ_1:def 3;
then reconsider i' = i as Element of dom g by Def12;
g . i' is AbGroup ;
hence g . i is AbGroup ; :: thesis: verum