let A be QC-alphabet ; :: thesis: for n being Nat
for F being Element of QC-WFF A
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 A st
( G = (tree_of_subformulae F) . (t ^ <*n*>) & G is_immediate_constituent_of (tree_of_subformulae F) . t )
let n be Nat; :: thesis: for F being Element of QC-WFF A
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 A 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 A; :: 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 A 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 A st
( G = (tree_of_subformulae F) . (t ^ <*n*>) & G is_immediate_constituent_of (tree_of_subformulae F) . t ) )
A1: succ t = { (t ^ <*k*>) where k is Nat : t ^ <*k*> in dom (tree_of_subformulae F) } ;
assume t ^ <*n*> in dom (tree_of_subformulae F) ; :: thesis: 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 )
then consider t9 being Element of dom (tree_of_subformulae F) such that
A2: t9 = t ^ <*n*> ;
A3: rng (list_of_immediate_constituents ((tree_of_subformulae F) . t)) = { G1 where G1 is Element of QC-WFF A : G1 is_immediate_constituent_of (tree_of_subformulae F) . t } by Th4;
consider G being Element of QC-WFF A such that
A4: G = (tree_of_subformulae F) . t9 ;
t9 in { (t ^ <*k*>) where k is Nat : t ^ <*k*> in dom (tree_of_subformulae F) } by A2;
then G in rng (succ ((tree_of_subformulae F),t)) by A4, A1, TREES_9:41;
then G in rng (list_of_immediate_constituents ((tree_of_subformulae F) . t)) by Def2;
hence 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 A2, A4, A3; :: thesis: verum