for A being QC-alphabet
for F, G being Element of QC-WFF A
for s being FinSequence st @ F = (@ G) ^ s holds
@ F = @ G