let A be QC-alphabet ; :: thesis: for F being Element of QC-WFF A
for t being Element of dom (tree_of_subformulae F) st (tree_of_subformulae F) . t is negative holds
( t ^ <*0*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0*>) = the_argument_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 (tree_of_subformulae F) . t is negative holds
( t ^ <*0*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0*>) = the_argument_of ((tree_of_subformulae F) . t) )
let t be Element of dom (tree_of_subformulae F); :: thesis: ( (tree_of_subformulae F) . t is negative implies ( t ^ <*0*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0*>) = the_argument_of ((tree_of_subformulae F) . t) ) )
set G = (tree_of_subformulae F) . t;
consider H being Element of QC-WFF A such that
A1: H = the_argument_of ((tree_of_subformulae F) . t) ;
assume A2: (tree_of_subformulae F) . t is negative ; :: thesis: ( t ^ <*0*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0*>) = the_argument_of ((tree_of_subformulae F) . t) )
then H is_immediate_constituent_of (tree_of_subformulae F) . t by A1, QC_LANG2:48;
then consider m being Nat such that
A3: t ^ <*m*> in dom (tree_of_subformulae F) and
H = (tree_of_subformulae F) . (t ^ <*m*>) by Th7;
m = 0 by A2, A3, Th21;
hence ( t ^ <*0*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0*>) = the_argument_of ((tree_of_subformulae F) . t) ) by A2, A3, Th21; :: thesis: verum