let G, F be Element of QC-WFF ; :: thesis: ( G in rng (tree_of_subformulae F) iff G is_subformula_of F )

now

set T = dom (tree_of_subformulae F);
defpred S₁[ set ] means ex H being Element of QC-WFF st
( (tree_of_subformulae F) . $1 = H & H is_subformula_of F );
assume G in rng (tree_of_subformulae F) ; :: thesis: G is_subformula_of F
then consider t being set such that
A1: t in dom (tree_of_subformulae F) and
A2: (tree_of_subformulae F) . t = G by FUNCT_1:def 3;
reconsider t = t as Element of dom (tree_of_subformulae F) by A1;
A3: for t being Element of dom (tree_of_subformulae F)
for n being Element of NAT st S₁[t] & t ^ <*n*> in dom (tree_of_subformulae F) holds
S₁[t ^ <*n*>]

proof

let t be Element of dom (tree_of_subformulae F); :: thesis: for n being Element of NAT st S₁[t] & t ^ <*n*> in dom (tree_of_subformulae F) holds
S₁[t ^ <*n*>]
let n be Element of NAT ; :: thesis: ( S₁[t] & t ^ <*n*> in dom (tree_of_subformulae F) implies S₁[t ^ <*n*>] )
assume that
A4: S₁[t] and
A5: t ^ <*n*> in dom (tree_of_subformulae F) ; :: thesis: S₁[t ^ <*n*>]
(tree_of_subformulae F) . (t ^ <*n*>) is Element of QC-WFF by A5, FUNCT_1:102;
then consider H9 being Element of QC-WFF such that
A6: (tree_of_subformulae F) . (t ^ <*n*>) = H9 ;
consider H being Element of QC-WFF such that
A7: (tree_of_subformulae F) . t = H and
A8: H is_subformula_of F by A4;
ex G9 being Element of QC-WFF st
( G9 = (tree_of_subformulae F) . (t ^ <*n*>) & G9 is_immediate_constituent_of (tree_of_subformulae F) . t ) by A5, Th35;
then H9 is_subformula_of H by A7, A6, QC_LANG2:52;
hence S₁[t ^ <*n*>] by A8, A6, QC_LANG2:57; :: thesis: verum

end;

A9: S₁[ {} ]

proof

take F ; :: thesis: ( (tree_of_subformulae F) . {} = F & F is_subformula_of F )
thus ( (tree_of_subformulae F) . {} = F & F is_subformula_of F ) by Def2; :: thesis: verum

end;

for t being Element of dom (tree_of_subformulae F) holds S₁[t] from TREES_2:sch 1(A9, A3);
then ex H being Element of QC-WFF st
( (tree_of_subformulae F) . t = H & H is_subformula_of F ) ;
hence G is_subformula_of F by A2; :: thesis: verum

end;

hence ( G in rng (tree_of_subformulae F) implies G is_subformula_of F ) ; :: thesis: ( G is_subformula_of F implies G in rng (tree_of_subformulae F) )
assume G is_subformula_of F ; :: thesis: G in rng (tree_of_subformulae F)
hence G in rng (tree_of_subformulae F) by Th34, Th38; :: thesis: verum