for A being QC-alphabet
for k being Nat
for F, G being Element of QC-WFF A st k in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . k holds
G is_immediate_constituent_of F