let m be Element of NAT ; :: thesis: for F being Element of QC-WFF
for t', t being Element of dom (tree_of_subformulae F) st t' = t ^ <*m*> & (tree_of_subformulae F) . t is universal holds
( (tree_of_subformulae F) . t' = the_scope_of ((tree_of_subformulae F) . t) & m = 0 )
let F be Element of QC-WFF ; :: thesis: for t', t being Element of dom (tree_of_subformulae F) st t' = t ^ <*m*> & (tree_of_subformulae F) . t is universal holds
( (tree_of_subformulae F) . t' = the_scope_of ((tree_of_subformulae F) . t) & m = 0 )
let t', t be Element of dom (tree_of_subformulae F); :: thesis: ( t' = t ^ <*m*> & (tree_of_subformulae F) . t is universal implies ( (tree_of_subformulae F) . t' = the_scope_of ((tree_of_subformulae F) . t) & m = 0 ) )
set G = (tree_of_subformulae F) . t;
set H = (tree_of_subformulae F) . t';
assume A1: ( t' = t ^ <*m*> & (tree_of_subformulae F) . t is universal ) ; :: thesis: ( (tree_of_subformulae F) . t' = the_scope_of ((tree_of_subformulae F) . t) & m = 0 )
then A2: (tree_of_subformulae F) . t' is_immediate_constituent_of (tree_of_subformulae F) . t by Th36;
A3: succ (tree_of_subformulae F),t = list_of_immediate_constituents ((tree_of_subformulae F) . t) by Def2;
( (tree_of_subformulae F) . t <> VERUM & 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 A1, QC_LANG1:51;
then A4: list_of_immediate_constituents ((tree_of_subformulae F) . t) = <*(the_scope_of ((tree_of_subformulae F) . t))*> by Def1;
consider q being Element of dom (tree_of_subformulae F) such that
A5: ( q = t & succ (tree_of_subformulae F),t = (tree_of_subformulae F) * (q succ ) ) by TREES_9:def 6;
dom <*(the_scope_of ((tree_of_subformulae F) . t))*> = dom (t succ ) by A3, A4, A5, Th10;
then A6: m + 1 in dom <*(the_scope_of ((tree_of_subformulae F) . t))*> by A1, Th12;
dom <*(the_scope_of ((tree_of_subformulae F) . t))*> = Seg 1 by FINSEQ_1:def 8;
then m + 1 = 0 + 1 by A6, FINSEQ_1:4, TARSKI:def 1;
hence ( (tree_of_subformulae F) . t' = the_scope_of ((tree_of_subformulae F) . t) & m = 0 ) by A1, A2, QC_LANG2:67; :: thesis: verum