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 conjunctive & not ( (tree_of_subformulae F) . t9 = the_left_argument_of ((tree_of_subformulae F) . t) & m = 0 ) holds
( (tree_of_subformulae F) . t9 = the_right_argument_of ((tree_of_subformulae F) . t) & m = 1 )
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 conjunctive & not ( (tree_of_subformulae F) . t9 = the_left_argument_of ((tree_of_subformulae F) . t) & m = 0 ) holds
( (tree_of_subformulae F) . t9 = the_right_argument_of ((tree_of_subformulae F) . t) & m = 1 )
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 conjunctive & not ( (tree_of_subformulae F) . t9 = the_left_argument_of ((tree_of_subformulae F) . t) & m = 0 ) holds
( (tree_of_subformulae F) . t9 = the_right_argument_of ((tree_of_subformulae F) . t) & m = 1 )
let t, t9 be Element of dom (tree_of_subformulae F); :: thesis: ( t9 = t ^ <*m*> & (tree_of_subformulae F) . t is conjunctive & not ( (tree_of_subformulae F) . t9 = the_left_argument_of ((tree_of_subformulae F) . t) & m = 0 ) implies ( (tree_of_subformulae F) . t9 = the_right_argument_of ((tree_of_subformulae F) . t) & m = 1 ) )
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 conjunctive ; :: thesis: ( ( (tree_of_subformulae F) . t9 = the_left_argument_of ((tree_of_subformulae F) . t) & m = 0 ) or ( (tree_of_subformulae F) . t9 = the_right_argument_of ((tree_of_subformulae F) . t) & m = 1 ) )
A3: list_of_immediate_constituents ((tree_of_subformulae F) . t) = <*(the_left_argument_of ((tree_of_subformulae F) . t)),(the_right_argument_of ((tree_of_subformulae F) . t))*> by A2, Def1;
len <*(the_left_argument_of ((tree_of_subformulae F) . t)),(the_right_argument_of ((tree_of_subformulae F) . t))*> = 2 by FINSEQ_1:44;
then A4: dom <*(the_left_argument_of ((tree_of_subformulae F) . t)),(the_right_argument_of ((tree_of_subformulae F) . t))*> = Seg 2 by FINSEQ_1:def 3;
A5: succ ((tree_of_subformulae F),t) = list_of_immediate_constituents ((tree_of_subformulae F) . t) by Def2;
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 TREES_9:def 6;
then dom <*(the_left_argument_of ((tree_of_subformulae F) . t)),(the_right_argument_of ((tree_of_subformulae F) . t))*> = dom (t succ) by A5, A3, TREES_9:37;
then m + 1 in dom <*(the_left_argument_of ((tree_of_subformulae F) . t)),(the_right_argument_of ((tree_of_subformulae F) . t))*> by A1, TREES_9:39;
then A6: ( m + 1 = 0 + 1 or m + 1 = 1 + 1 ) by A4, FINSEQ_1:2, TARSKI:def 2;