Carrier <*G,A*> = <* the carrier of G, the carrier of A*> by PRALG_1:18;
then A1: Carrier <*G,A*> is finite ;
for x being set st x in rng (Carrier <*G,A*>) holds
x is finite

proof

let x be set ; :: thesis: ( x in rng (Carrier <*G,A*>) implies x is finite )
assume x in rng (Carrier <*G,A*>) ; :: thesis: x is finite
then consider i being object such that
A2: ( i in dom (Carrier <*G,A*>) & x = (Carrier <*G,A*>) . i ) by FUNCT_1:def 3;

per cases ( i = 1 or i = 2 ) by A2, TARSKI:def 2;

suppose i = 1 ; :: thesis: x is finite

then x = <* the carrier of G, the carrier of A*> . 1 by A2, PRALG_1:18
.= the carrier of G ;
hence x is finite ; :: thesis: verum

end;

suppose i = 2 ; :: thesis: x is finite

then x = <* the carrier of G, the carrier of A*> . 2 by A2, PRALG_1:18
.= the carrier of A ;
hence x is finite ; :: thesis: verum

end;

end;

end;

then ( Carrier <*G,A*> is finite & Carrier <*G,A*> is finite-yielding ) by A1, FINSET_1:def 2;
then product (Carrier <*G,A*>) is finite ;
hence semidirect_product (G,A,phi) is finite by Def1; :: thesis: verum