let F be Element of QC-WFF ; :: thesis: F in rng (tree_of_subformulae F)
( (tree_of_subformulae F) . {} = F & {} in dom (tree_of_subformulae F) ) by Def2, TREES_1:47;
hence F in rng (tree_of_subformulae F) by FUNCT_1:def 5; :: thesis: verum