let A be QC-alphabet ; :: thesis: for F, H being Element of QC-WFF A
for t being Element of dom (tree_of_subformulae F) holds
( H is_immediate_constituent_of (tree_of_subformulae F) . t iff ex n being Nat st
( t ^ <*n*> in dom (tree_of_subformulae F) & H = (tree_of_subformulae F) . (t ^ <*n*>) ) )
let F, H be Element of QC-WFF A; :: thesis: for t being Element of dom (tree_of_subformulae F) holds
( H is_immediate_constituent_of (tree_of_subformulae F) . t iff ex n being Nat st
( t ^ <*n*> in dom (tree_of_subformulae F) & H = (tree_of_subformulae F) . (t ^ <*n*>) ) )
let t be Element of dom (tree_of_subformulae F); :: thesis: ( H is_immediate_constituent_of (tree_of_subformulae F) . t iff ex n being Nat st
( t ^ <*n*> in dom (tree_of_subformulae F) & H = (tree_of_subformulae F) . (t ^ <*n*>) ) )

now :: thesis: ( H is_immediate_constituent_of (tree_of_subformulae F) . t implies ex n being Nat st
( t ^ <*n*> in dom (tree_of_subformulae F) & H = (tree_of_subformulae F) . (t ^ <*n*>) ) )

set G = (tree_of_subformulae F) . t;
assume H is_immediate_constituent_of (tree_of_subformulae F) . t ; :: thesis: ex n being Nat st
( t ^ <*n*> in dom (tree_of_subformulae F) & H = (tree_of_subformulae F) . (t ^ <*n*>) )
then H in { H1 where H1 is Element of QC-WFF A : H1 is_immediate_constituent_of (tree_of_subformulae F) . t } ;
then A1: H in rng (list_of_immediate_constituents ((tree_of_subformulae F) . t)) by Th4;
succ ((tree_of_subformulae F),t) = list_of_immediate_constituents ((tree_of_subformulae F) . t) by Def2;
then consider t9 being Element of dom (tree_of_subformulae F) such that
A2: H = (tree_of_subformulae F) . t9 and
A3: t9 in succ t by A1, TREES_9:42;
ex n being Nat st
( t9 = t ^ <*n*> & t ^ <*n*> in dom (tree_of_subformulae F) ) by A3;
hence ex n being Nat st
( t ^ <*n*> in dom (tree_of_subformulae F) & H = (tree_of_subformulae F) . (t ^ <*n*>) ) by A2; :: thesis: verum

end;

hence ( H is_immediate_constituent_of (tree_of_subformulae F) . t implies ex n being Nat st
( t ^ <*n*> in dom (tree_of_subformulae F) & H = (tree_of_subformulae F) . (t ^ <*n*>) ) ) ; :: thesis: ( ex n being Nat st
( t ^ <*n*> in dom (tree_of_subformulae F) & H = (tree_of_subformulae F) . (t ^ <*n*>) ) implies H is_immediate_constituent_of (tree_of_subformulae F) . t )
given n being Nat such that A4: t ^ <*n*> in dom (tree_of_subformulae F) and
A5: H = (tree_of_subformulae F) . (t ^ <*n*>) ; :: thesis: H is_immediate_constituent_of (tree_of_subformulae F) . t
ex G being Element of QC-WFF A st
( G = (tree_of_subformulae F) . (t ^ <*n*>) & G is_immediate_constituent_of (tree_of_subformulae F) . t ) by A4, Th6;
hence H is_immediate_constituent_of (tree_of_subformulae F) . t by A5; :: thesis: verum