let x be set ; for T being DecoratedTree holds x -tree <*T*> = ((elementary_tree 1) --> x) with-replacement <*0 *>,T
let T be DecoratedTree; x -tree <*T*> = ((elementary_tree 1) --> x) with-replacement <*0 *>,T
set D = ((elementary_tree 1) --> x) with-replacement <*0 *>,T;
set W = (elementary_tree 1) with-replacement <*0 *>,(dom T);
A1: dom (x -tree <*T*>) =
tree (doms <*T*>)
by Th10
.=
tree <*(dom T)*>
by FUNCT_6:33
.=
^ (dom T)
by TREES_3:def 16
.=
(elementary_tree 1) with-replacement <*0 *>,(dom T)
by TREES_3:61
;
A2:
dom ((elementary_tree 1) --> x) = elementary_tree 1
by FUNCOP_1:19;
reconsider t1 = {} , t2 = <*0 *> as Element of elementary_tree 1 by TARSKI:def 2, TREES_1:88;
A3:
t2 = t2
;
A4:
dom (((elementary_tree 1) --> x) with-replacement <*0 *>,T) = (elementary_tree 1) with-replacement <*0 *>,(dom T)
by A2, A3, TREES_2:def 12;
A5:
{} in dom T
by TREES_1:47;
A6:
now let y be
set ;
( y in (elementary_tree 1) with-replacement <*0 *>,(dom T) implies (((elementary_tree 1) --> x) with-replacement <*0 *>,T) . y = (x -tree <*T*>) . y )assume A7:
y in (elementary_tree 1) with-replacement <*0 *>,
(dom T)
;
(((elementary_tree 1) --> x) with-replacement <*0 *>,T) . y = (x -tree <*T*>) . yreconsider q =
y as
Element of
(elementary_tree 1) with-replacement <*0 *>,
(dom T) by A7;
A8:
(
q in elementary_tree 1 or ex
v being
FinSequence of
NAT st
(
v in dom T &
q = t2 ^ v ) )
by TREES_1:def 12;
A9:
(
q = {} or (
q = t2 &
t2 = t2 ^ t1 ) or ex
v being
FinSequence of
NAT st
(
v in dom T &
q = <*0 *> ^ v ) )
by A8, FINSEQ_1:47, TARSKI:def 2, TREES_1:88;
A10:
not
t2 is_a_prefix_of t1
;
A11:
(((elementary_tree 1) --> x) with-replacement <*0 *>,T) . {} =
((elementary_tree 1) --> x) . t1
by A2, A10, TREES_3:48
.=
x
by FUNCOP_1:13
.=
(x -tree <*T*>) . {}
by Def4
;
A12:
now given r being
FinSequence of
NAT such that A13:
r in dom T
and A14:
q = <*0 *> ^ r
;
(((elementary_tree 1) --> x) with-replacement <*0 *>,T) . q = (x -tree <*T*>) . qreconsider r =
r as
Node of
T by A13;
A15:
q = t2 ^ r
by A14;
A16:
(((elementary_tree 1) --> x) with-replacement <*0 *>,T) . q = T . r
by A2, A15, TREES_3:49;
A17:
(
len <*T*> = 1 &
<*T*> . (0 + 1) = T )
by FINSEQ_1:57;
A18:
(x -tree <*T*>) | t2 = T
by A17, Def4;
A19:
((elementary_tree 1) with-replacement <*0 *>,(dom T)) | t2 = dom T
by TREES_1:66;
thus
(((elementary_tree 1) --> x) with-replacement <*0 *>,T) . q = (x -tree <*T*>) . q
by A1, A14, A16, A18, A19, TREES_2:def 11;
verum end; thus
(((elementary_tree 1) --> x) with-replacement <*0 *>,T) . y = (x -tree <*T*>) . y
by A5, A9, A11, A12;
verum end;
thus
x -tree <*T*> = ((elementary_tree 1) --> x) with-replacement <*0 *>,T
by A1, A4, A6, FUNCT_1:9; verum