for b1 being Element of (semidirect_product (G,A,phi)) holds b1 is FinSequence-like

proof

let b1 be Element of (semidirect_product (G,A,phi)); :: thesis: b1 is FinSequence-like
b1 is Element of product (Carrier <*G,A*>) by Def1;
hence b1 is FinSequence-like ; :: thesis: verum

end;

hence for b₁ being Element of (semidirect_product (G,A,phi)) holds b₁ is FinSequence-like ; :: thesis: verum