the carrier of (SymGroup X) = permutations X by Def2;
hence the carrier of (SymGroup X) is finite ; :: according to STRUCT_0:def 11 :: thesis: verum