let A be QC-alphabet ; :: thesis: for F being Element of QC-WFF A
for t being Element of dom (tree_of_subformulae F) st (tree_of_subformulae F) . t is universal holds
( t ^ <*0*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0*>) = the_scope_of ((tree_of_subformulae F) . t) )
let F be Element of QC-WFF A; :: thesis: for t being Element of dom (tree_of_subformulae F) st (tree_of_subformulae F) . t is universal holds
( t ^ <*0*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0*>) = the_scope_of ((tree_of_subformulae F) . t) )
let t be Element of dom (tree_of_subformulae F); :: thesis: ( (tree_of_subformulae F) . t is universal implies ( t ^ <*0*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0*>) = the_scope_of ((tree_of_subformulae F) . t) ) )
set G = (tree_of_subformulae F) . t;
consider H being Element of QC-WFF A such that
A1: H = the_scope_of ((tree_of_subformulae F) . t) ;
assume A2: (tree_of_subformulae F) . t is universal ; :: thesis: ( t ^ <*0*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0*>) = the_scope_of ((tree_of_subformulae F) . t) )
then H is_immediate_constituent_of (tree_of_subformulae F) . t by A1, QC_LANG2:50;
then consider m being Nat such that
A3: t ^ <*m*> in dom (tree_of_subformulae F) and
H = (tree_of_subformulae F) . (t ^ <*m*>) by Th7;
m = 0 by A2, A3, Th23;
hence ( t ^ <*0*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0*>) = the_scope_of ((tree_of_subformulae F) . t) ) by A2, A3, Th23; :: thesis: verum