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