let A be QC-alphabet ; :: thesis: for m being Nat
for F being Element of QC-WFF A
for t, t9 being Element of dom (tree_of_subformulae F) st t9 = t ^ <*m*> & (tree_of_subformulae F) . t is negative holds
( (tree_of_subformulae F) . t9 = the_argument_of ((tree_of_subformulae F) . t) & m = 0 )
let m be Nat; :: thesis: for F being Element of QC-WFF A
for t, t9 being Element of dom (tree_of_subformulae F) st t9 = t ^ <*m*> & (tree_of_subformulae F) . t is negative holds
( (tree_of_subformulae F) . t9 = the_argument_of ((tree_of_subformulae F) . t) & m = 0 )
let F be Element of QC-WFF A; :: thesis: for t, t9 being Element of dom (tree_of_subformulae F) st t9 = t ^ <*m*> & (tree_of_subformulae F) . t is negative holds
( (tree_of_subformulae F) . t9 = the_argument_of ((tree_of_subformulae F) . t) & m = 0 )
let t, t9 be Element of dom (tree_of_subformulae F); :: thesis: ( t9 = t ^ <*m*> & (tree_of_subformulae F) . t is negative implies ( (tree_of_subformulae F) . t9 = the_argument_of ((tree_of_subformulae F) . t) & m = 0 ) )
set G = (tree_of_subformulae F) . t;
set H = (tree_of_subformulae F) . t9;
assume that
A1: t9 = t ^ <*m*> and
A2: (tree_of_subformulae F) . t is negative ; :: thesis: ( (tree_of_subformulae F) . t9 = the_argument_of ((tree_of_subformulae F) . t) & m = 0 )
A3: dom <*(the_argument_of ((tree_of_subformulae F) . t))*> = Seg 1 by FINSEQ_1:def 8;
A4: ( succ ((tree_of_subformulae F),t) = list_of_immediate_constituents ((tree_of_subformulae F) . t) & ex q being Element of dom (tree_of_subformulae F) st
( q = t & succ ((tree_of_subformulae F),t) = (tree_of_subformulae F) * (q succ) ) ) by Def2, TREES_9:def 6;
list_of_immediate_constituents ((tree_of_subformulae F) . t) = <*(the_argument_of ((tree_of_subformulae F) . t))*> by A2, Def1;
then dom <*(the_argument_of ((tree_of_subformulae F) . t))*> = dom (t succ) by A4, TREES_9:37;
then m + 1 in dom <*(the_argument_of ((tree_of_subformulae F) . t))*> by A1, TREES_9:39;
then A5: m + 1 = 0 + 1 by A3, FINSEQ_1:2, TARSKI:def 1;
(tree_of_subformulae F) . t9 is_immediate_constituent_of (tree_of_subformulae F) . t by A1, Th7;
hence ( (tree_of_subformulae F) . t9 = the_argument_of ((tree_of_subformulae F) . t) & m = 0 ) by A2, A5, QC_LANG2:48; :: thesis: verum