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 conjunctive holds
( t ^ <*0 *> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0 *>) = the_left_argument_of ((tree_of_subformulae F) . t) & t ^ <*1*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*1*>) = the_right_argument_of ((tree_of_subformulae F) . t) )
let t be Element of dom (tree_of_subformulae F); :: thesis: ( (tree_of_subformulae F) . t is conjunctive implies ( t ^ <*0 *> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0 *>) = the_left_argument_of ((tree_of_subformulae F) . t) & t ^ <*1*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*1*>) = the_right_argument_of ((tree_of_subformulae F) . t) ) )
set G = (tree_of_subformulae F) . t;
assume A1: (tree_of_subformulae F) . t is conjunctive ; :: thesis: ( t ^ <*0 *> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0 *>) = the_left_argument_of ((tree_of_subformulae F) . t) & t ^ <*1*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*1*>) = the_right_argument_of ((tree_of_subformulae F) . t) )
(tree_of_subformulae F) * (t succ ) = succ (tree_of_subformulae F),t

proof

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;
hence (tree_of_subformulae F) * (t succ ) = succ (tree_of_subformulae F),t ; :: thesis: verum

end;

then A2: dom (t succ ) = dom (succ (tree_of_subformulae F),t) by Th10
.= dom (list_of_immediate_constituents ((tree_of_subformulae F) . t)) by Def2
.= dom <*(the_left_argument_of ((tree_of_subformulae F) . t)),(the_right_argument_of ((tree_of_subformulae F) . t))*> by A1, Def1
.= {1,2} by Lm1, FINSEQ_1:4 ;
A3: 0 + 1 in {1,2} by TARSKI:def 2;
then t ^ <*0 *> in dom (tree_of_subformulae F) by A2, Th12;
then (tree_of_subformulae F) . (t ^ <*0 *>) = (succ (tree_of_subformulae F),t) . (0 + 1) by Th13
.= (list_of_immediate_constituents ((tree_of_subformulae F) . t)) . 1 by Def2
.= <*(the_left_argument_of ((tree_of_subformulae F) . t)),(the_right_argument_of ((tree_of_subformulae F) . t))*> . 1 by A1, Def1
.= the_left_argument_of ((tree_of_subformulae F) . t) by FINSEQ_1:61 ;
hence ( t ^ <*0 *> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0 *>) = the_left_argument_of ((tree_of_subformulae F) . t) ) by A2, A3, Th12; :: thesis: ( t ^ <*1*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*1*>) = the_right_argument_of ((tree_of_subformulae F) . t) )
A4: 1 + 1 in {1,2} by TARSKI:def 2;
then t ^ <*1*> in dom (tree_of_subformulae F) by A2, Th12;
then (tree_of_subformulae F) . (t ^ <*1*>) = (succ (tree_of_subformulae F),t) . (1 + 1) by Th13
.= (list_of_immediate_constituents ((tree_of_subformulae F) . t)) . 2 by Def2
.= <*(the_left_argument_of ((tree_of_subformulae F) . t)),(the_right_argument_of ((tree_of_subformulae F) . t))*> . 2 by A1, Def1
.= the_right_argument_of ((tree_of_subformulae F) . t) by FINSEQ_1:61 ;
hence ( t ^ <*1*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*1*>) = the_right_argument_of ((tree_of_subformulae F) . t) ) by A2, A4, Th12; :: thesis: verum