let A be QC-alphabet ; :: thesis: for F being Element of QC-WFF A
for t being Element of dom (tree_of_subformulae F) holds (tree_of_subformulae F) | t = tree_of_subformulae ((tree_of_subformulae F) . t)
let F be Element of QC-WFF A; :: thesis: for t being Element of dom (tree_of_subformulae F) holds (tree_of_subformulae F) | t = tree_of_subformulae ((tree_of_subformulae F) . t)
let t be Element of dom (tree_of_subformulae F); :: thesis: (tree_of_subformulae F) | t = tree_of_subformulae ((tree_of_subformulae F) . t)
set T1 = (tree_of_subformulae F) | t;
set T2 = tree_of_subformulae ((tree_of_subformulae F) . t);
thus A1: dom ((tree_of_subformulae F) | t) = dom (tree_of_subformulae ((tree_of_subformulae F) . t)) :: according to TREES_4:def 1 :: thesis: for b₁ being Element of proj1 ((tree_of_subformulae F) | t) holds ((tree_of_subformulae F) | t) . b₁ = (tree_of_subformulae ((tree_of_subformulae F) . t)) . b₁

proof

let p be FinSequence of NAT ; :: according to TREES_2:def 1 :: thesis: ( ( not p in dom ((tree_of_subformulae F) | t) or p in dom (tree_of_subformulae ((tree_of_subformulae F) . t)) ) & ( not p in dom (tree_of_subformulae ((tree_of_subformulae F) . t)) or p in dom ((tree_of_subformulae F) | t) ) )

now :: thesis: ( p in dom ((tree_of_subformulae F) | t) implies p in dom (tree_of_subformulae ((tree_of_subformulae F) . t)) )

consider G being Element of QC-WFF A such that
A2: G = (tree_of_subformulae F) . t ;
A3: t in F -entry_points_in_subformula_tree_of G by A2, Def3;
consider t9 being FinSequence of NAT such that
A4: t9 = t ^ p ;
assume p in dom ((tree_of_subformulae F) | t) ; :: thesis: p in dom (tree_of_subformulae ((tree_of_subformulae F) . t))
then p in (dom (tree_of_subformulae F)) | t by TREES_2:def 10;
then reconsider t9 = t9 as Element of dom (tree_of_subformulae F) by A4, TREES_1:def 6;
consider H being Element of QC-WFF A such that
A5: H = (tree_of_subformulae F) . t9 ;
A6: G -entry_points_in_subformula_tree_of H c= dom (tree_of_subformulae ((tree_of_subformulae F) . t)) by A2, TREES_1:def 11;
t9 in F -entry_points_in_subformula_tree_of H by A5, Def3;
then p in G -entry_points_in_subformula_tree_of H by A3, A4, Th28;
hence p in dom (tree_of_subformulae ((tree_of_subformulae F) . t)) by A6; :: thesis: verum

end;

hence ( p in dom ((tree_of_subformulae F) | t) implies p in dom (tree_of_subformulae ((tree_of_subformulae F) . t)) ) ; :: thesis: ( not p in dom (tree_of_subformulae ((tree_of_subformulae F) . t)) or p in dom ((tree_of_subformulae F) | t) )

now :: thesis: ( p in dom (tree_of_subformulae ((tree_of_subformulae F) . t)) implies p in dom ((tree_of_subformulae F) | t) )

consider G being Element of QC-WFF A such that
A7: G = (tree_of_subformulae F) . t ;
assume p in dom (tree_of_subformulae ((tree_of_subformulae F) . t)) ; :: thesis: p in dom ((tree_of_subformulae F) | t)
then reconsider s = p as Element of dom (tree_of_subformulae G) by A7;
consider H being Element of QC-WFF A such that
A8: H = (tree_of_subformulae G) . s ;
A9: s in G -entry_points_in_subformula_tree_of H by A8, Def3;
A10: F -entry_points_in_subformula_tree_of H c= dom (tree_of_subformulae F) by TREES_1:def 11;
t in F -entry_points_in_subformula_tree_of G by A7, Def3;
then t ^ s in F -entry_points_in_subformula_tree_of H by A9, Th27;
then s in (dom (tree_of_subformulae F)) | t by A10, TREES_1:def 6;
hence p in dom ((tree_of_subformulae F) | t) by TREES_2:def 10; :: thesis: verum

end;

hence ( not p in dom (tree_of_subformulae ((tree_of_subformulae F) . t)) or p in dom ((tree_of_subformulae F) | t) ) ; :: thesis: verum

end;

now :: thesis: for p being Node of ((tree_of_subformulae F) | t) holds ((tree_of_subformulae F) | t) . p = (tree_of_subformulae ((tree_of_subformulae F) . t)) . p

let p be Node of ((tree_of_subformulae F) | t); :: thesis: ((tree_of_subformulae F) | t) . p = (tree_of_subformulae ((tree_of_subformulae F) . t)) . p
consider G being Element of QC-WFF A such that
A11: G = (tree_of_subformulae F) . t ;
reconsider s = p as Element of dom (tree_of_subformulae G) by A1, A11;
A12: dom ((tree_of_subformulae F) | t) = (dom (tree_of_subformulae F)) | t by TREES_2:def 10;
then reconsider t9 = t ^ s as Element of dom (tree_of_subformulae F) by TREES_1:def 6;
consider H being Element of QC-WFF A such that
A13: H = ((tree_of_subformulae F) | t) . p ;
A14: t in F -entry_points_in_subformula_tree_of G by A11, Def3;
((tree_of_subformulae F) | t) . p = (tree_of_subformulae F) . (t ^ p) by A12, TREES_2:def 10;
then t9 in F -entry_points_in_subformula_tree_of H by A13, Def3;
then s in G -entry_points_in_subformula_tree_of H by A14, Th28;
hence ((tree_of_subformulae F) | t) . p = (tree_of_subformulae ((tree_of_subformulae F) . t)) . p by A11, A13, Def3; :: thesis: verum

end;

hence for p being Node of ((tree_of_subformulae F) | t) holds ((tree_of_subformulae F) | t) . p = (tree_of_subformulae ((tree_of_subformulae F) . t)) . p ; :: thesis: verum