let F be Element of QC-WFF ; :: 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 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 Element of NAT such that
A3: t ^ <*m*> in dom (tree_of_subformulae F) and
H = (tree_of_subformulae F) . (t ^ <*m*>) by Th36;
m = 0 by A2, A3, Th51;
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, Th51; :: thesis: verum