<*G1,G2*> = <*G1*> ^ <*G2*> by FINSEQ_1:def 9;
hence <*G1,G2*> is _finite ; :: thesis: verum