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 universal holds
( (tree_of_subformulae F) . t9 = the_scope_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 universal holds
( (tree_of_subformulae F) . t9 = the_scope_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 universal holds
( (tree_of_subformulae F) . t9 = the_scope_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 universal implies ( (tree_of_subformulae F) . t9 = the_scope_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 universal ; :: thesis: ( (tree_of_subformulae F) . t9 = the_scope_of ((tree_of_subformulae F) . t) & m = 0 )
A3: dom <*(the_scope_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;
not VERUM A is universal by QC_LANG1:20;
then A5: (tree_of_subformulae F) . t <> VERUM A by A2;
( not (tree_of_subformulae F) . t is atomic & not (tree_of_subformulae F) . t is negative & not (tree_of_subformulae F) . t is conjunctive ) by A2, QC_LANG1:20;
then list_of_immediate_constituents ((tree_of_subformulae F) . t) = <*(the_scope_of ((tree_of_subformulae F) . t))*> by Def1, A5;
then dom <*(the_scope_of ((tree_of_subformulae F) . t))*> = dom (t succ) by A4, TREES_9:37;
then m + 1 in dom <*(the_scope_of ((tree_of_subformulae F) . t))*> by A1, TREES_9:39;
then A6: 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_scope_of ((tree_of_subformulae F) . t) & m = 0 ) by A2, A6, QC_LANG2:50; :: thesis: verum