let A be QC-alphabet ; :: thesis: for F being Element of QC-WFF A holds F in rng (tree_of_subformulae F)
let F be Element of QC-WFF A; :: thesis: F in rng (tree_of_subformulae F)
( (tree_of_subformulae F) . {} = F & {} in dom (tree_of_subformulae F) ) by Def2, TREES_1:22;
hence F in rng (tree_of_subformulae F) by FUNCT_1:def 3; :: thesis: verum