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