per cases ( n is Nat or n = +infty ) by COUNTERS:2;

suppose n is Nat ; :: thesis: ex b₁ being strict Group st
( ( n = +infty implies b₁ = semidirect_product (INT.Group,(INT.Group 2),(inversions INT.Group)) ) & ( n <> +infty implies ex n1 being non zero Nat st
( n = n1 & b₁ = semidirect_product ((INT.Group n1),(INT.Group 2),(inversions (INT.Group n1))) ) ) )

then reconsider n1 = n as non zero Nat ;
take G = semidirect_product ((INT.Group n1),(INT.Group 2),(inversions (INT.Group n1))); :: thesis: ( ( n = +infty implies G = semidirect_product (INT.Group,(INT.Group 2),(inversions INT.Group)) ) & ( n <> +infty implies ex n1 being non zero Nat st
( n = n1 & G = semidirect_product ((INT.Group n1),(INT.Group 2),(inversions (INT.Group n1))) ) ) )
thus ( ( n = +infty implies G = semidirect_product (INT.Group,(INT.Group 2),(inversions INT.Group)) ) & ( n <> +infty implies ex n1 being non zero Nat st
( n = n1 & G = semidirect_product ((INT.Group n1),(INT.Group 2),(inversions (INT.Group n1))) ) ) ) ; :: thesis: verum

end;

suppose n = +infty ; :: thesis: ex b₁ being strict Group st
( ( n = +infty implies b₁ = semidirect_product (INT.Group,(INT.Group 2),(inversions INT.Group)) ) & ( n <> +infty implies ex n1 being non zero Nat st
( n = n1 & b₁ = semidirect_product ((INT.Group n1),(INT.Group 2),(inversions (INT.Group n1))) ) ) )

hence ex b₁ being strict Group st
( ( n = +infty implies b₁ = semidirect_product (INT.Group,(INT.Group 2),(inversions INT.Group)) ) & ( n <> +infty implies ex n1 being non zero Nat st
( n = n1 & b₁ = semidirect_product ((INT.Group n1),(INT.Group 2),(inversions (INT.Group n1))) ) ) ) ; :: thesis: verum

end;

end;