the carrier' of (StandardStackSystem A) = A * by Def7;
hence the carrier' of (StandardStackSystem A) is functional ; :: thesis: verum