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 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;
assume A1: (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) )
consider H being Element of QC-WFF ;
consider H being Element of QC-WFF such that
A2: H = the_scope_of ((tree_of_subformulae F) . t) ;
H is_immediate_constituent_of (tree_of_subformulae F) . t by A1, A2, QC_LANG2:67;
then consider m being Element of NAT such that
A3: ( t ^ <*m*> in dom (tree_of_subformulae F) & H = (tree_of_subformulae F) . (t ^ <*m*>) ) by Th36;
consider t' being Element of dom (tree_of_subformulae F) such that
A4: t' = t ^ <*m*> by A3;
( (tree_of_subformulae F) . t' = the_scope_of ((tree_of_subformulae F) . t) & m = 0 ) by A1, A4, Th53;
hence ( t ^ <*0 *> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0 *>) = the_scope_of ((tree_of_subformulae F) . t) ) by A4; :: thesis: verum