let A be QC-alphabet ; 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; 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; 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); ( 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
; ( ( (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;