the carrier' of (StandardStackSystem A) = A * by Def7;
hence for b₁ being stack of (StandardStackSystem A) holds b₁ is FinSequence-like ; :: thesis: verum