for Al being QC-alphabet
for c, d being object
for f being FinSequence of CQC-WFF Al holds
( 1 in dom <*c,d*> & 2 in dom <*c,d*> & (f ^ <*c,d*>) . ((len f) + 1) = c & (f ^ <*c,d*>) . ((len f) + 2) = d )