let n be Element of NAT ; :: thesis: for F being Element of QC-WFF
for t being Element of dom (tree_of_subformulae F) st t ^ <*n*> in dom (tree_of_subformulae F) holds
ex G being Element of QC-WFF st
( G = (tree_of_subformulae F) . (t ^ <*n*>) & G is_immediate_constituent_of (tree_of_subformulae F) . t )
let F be Element of QC-WFF ; :: thesis: for t being Element of dom (tree_of_subformulae F) st t ^ <*n*> in dom (tree_of_subformulae F) holds
ex G being Element of QC-WFF st
( G = (tree_of_subformulae F) . (t ^ <*n*>) & G is_immediate_constituent_of (tree_of_subformulae F) . t )
let t be Element of dom (tree_of_subformulae F); :: thesis: ( t ^ <*n*> in dom (tree_of_subformulae F) implies ex G being Element of QC-WFF st
( G = (tree_of_subformulae F) . (t ^ <*n*>) & G is_immediate_constituent_of (tree_of_subformulae F) . t ) )
assume t ^ <*n*> in dom (tree_of_subformulae F) ; :: thesis: ex G being Element of QC-WFF st
( G = (tree_of_subformulae F) . (t ^ <*n*>) & G is_immediate_constituent_of (tree_of_subformulae F) . t )
then consider t' being Element of dom (tree_of_subformulae F) such that
A1: t' = t ^ <*n*> ;
consider G being Element of QC-WFF such that
A2: G = (tree_of_subformulae F) . t' ;
A3: succ t = { (t ^ <*k*>) where k is Element of NAT : t ^ <*k*> in dom (tree_of_subformulae F) } ;
t' in { (t ^ <*k*>) where k is Element of NAT : t ^ <*k*> in dom (tree_of_subformulae F) } by A1;
then G in rng (succ (tree_of_subformulae F),t) by A2, A3, Th14;
then A4: G in rng (list_of_immediate_constituents ((tree_of_subformulae F) . t)) by Def2;
rng (list_of_immediate_constituents ((tree_of_subformulae F) . t)) = { G1 where G1 is Element of QC-WFF : G1 is_immediate_constituent_of (tree_of_subformulae F) . t } by Th31;
then consider G' being Element of QC-WFF such that
A5: ( G' = G & G' is_immediate_constituent_of (tree_of_subformulae F) . t ) by A4;
thus ex G being Element of QC-WFF st
( G = (tree_of_subformulae F) . (t ^ <*n*>) & G is_immediate_constituent_of (tree_of_subformulae F) . t ) by A1, A2, A5; :: thesis: verum