:: deftheorem Def34 defines AL-correct AOFA_L00:def 38 :
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S being non empty non void b₁ -extension AlgLangSignature over Union X
for Y being b₃ -tolerating ManySortedSet of the carrier of S
for L being BialgebraStr over S,Y holds
( L is AL-correct iff the carrier of L = the Sorts of L . the program-sort of S );