defpred S₁[ set ] means ( $1 in Leaves (dom T) & T . $1 = x );
consider W being Tree such that
A1: for p being FinSequence holds
( p in W iff ( p in dom T or ex q being Node of T ex r being Node of T9 st
( S₁[q] & p = q ^ r ) ) ) from TREES_4:sch 1();
defpred S₂[ object , object ] means ( ( $1 is Node of T & ( not $1 in Leaves (dom T) or T . $1 <> x ) & $2 = T . $1 ) or ex p being Node of T ex q being Node of T9 st
( $1 = p ^ q & p in Leaves (dom T) & T . p = x & $2 = T9 . q ) );
A2: for z being object st z in W holds
ex y being object st S₂[z,y]

proof

let z be object ; :: thesis: ( z in W implies ex y being object st S₂[z,y] )
assume z in W ; :: thesis: ex y being object st S₂[z,y]
then reconsider w = z as Element of W ;

A3: now :: thesis: ( ex q being Node of T ex r being Node of T9 st
( q in Leaves (dom T) & T . q = x & w = q ^ r ) implies ex y being set ex q being Node of T ex r being Node of T9 st
( z = q ^ r & q in Leaves (dom T) & T . q = x & y = T9 . r ) )

given q being Node of T, r being Node of T9 such that A4: ( q in Leaves (dom T) & T . q = x & w = q ^ r ) ; :: thesis: ex y being set ex q being Node of T ex r being Node of T9 st
( z = q ^ r & q in Leaves (dom T) & T . q = x & y = T9 . r )
take y = T9 . r; :: thesis: ex q being Node of T ex r being Node of T9 st
( z = q ^ r & q in Leaves (dom T) & T . q = x & y = T9 . r )
take q = q; :: thesis: ex r being Node of T9 st
( z = q ^ r & q in Leaves (dom T) & T . q = x & y = T9 . r )
take r = r; :: thesis: ( z = q ^ r & q in Leaves (dom T) & T . q = x & y = T9 . r )
thus ( z = q ^ r & q in Leaves (dom T) & T . q = x & y = T9 . r ) by A4; :: thesis: verum

end;

now :: thesis: ( ( for q being Node of T
for r being Node of T9 holds
( not q in Leaves (dom T) or not T . q = x or not w = q ^ r ) ) implies ex y being set st
( z is Node of T & ( not z in Leaves (dom T) or T . z <> x ) & y = T . z ) )

assume A5: for q being Node of T
for r being Node of T9 holds
( not q in Leaves (dom T) or not T . q = x or not w = q ^ r ) ; :: thesis: ex y being set st
( z is Node of T & ( not z in Leaves (dom T) or T . z <> x ) & y = T . z )
take y = T . z; :: thesis: ( z is Node of T & ( not z in Leaves (dom T) or T . z <> x ) & y = T . z )
thus z is Node of T by A1, A5; :: thesis: ( ( not z in Leaves (dom T) or T . z <> x ) & y = T . z )
reconsider w = w as Node of T by A1, A5;
reconsider e = {} as Node of T9 by TREES_1:22;
w ^ e = w by FINSEQ_1:34;
hence ( ( not z in Leaves (dom T) or T . z <> x ) & y = T . z ) by A5; :: thesis: verum

end;

hence ex y being object st S₂[z,y] by A3; :: thesis: verum

end;

consider f being Function such that
A6: ( dom f = W & ( for z being object st z in W holds
S₂[z,f . z] ) ) from CLASSES1:sch 1(A2);
reconsider f = f as DecoratedTree by A6, TREES_2:def 8;
take f ; :: thesis: ( ( for p being FinSequence holds
( p in dom f iff ( p in dom T or ex q being Node of T ex r being Node of T9 st
( q in Leaves (dom T) & T . q = x & p = q ^ r ) ) ) ) & ( for p being Node of T st ( not p in Leaves (dom T) or T . p <> x ) holds
f . p = T . p ) & ( for p being Node of T
for q being Node of T9 st p in Leaves (dom T) & T . p = x holds
f . (p ^ q) = T9 . q ) )
thus for p being FinSequence holds
( p in dom f iff ( p in dom T or ex q being Node of T ex r being Node of T9 st
( q in Leaves (dom T) & T . q = x & p = q ^ r ) ) ) by A1, A6; :: thesis: ( ( for p being Node of T st ( not p in Leaves (dom T) or T . p <> x ) holds
f . p = T . p ) & ( for p being Node of T
for q being Node of T9 st p in Leaves (dom T) & T . p = x holds
f . (p ^ q) = T9 . q ) )
thus for p being Node of T st ( not p in Leaves (dom T) or T . p <> x ) holds
f . p = T . p :: thesis: for p being Node of T
for q being Node of T9 st p in Leaves (dom T) & T . p = x holds
f . (p ^ q) = T9 . q

proof

let p be Node of T; :: thesis: ( ( not p in Leaves (dom T) or T . p <> x ) implies f . p = T . p )
assume A7: ( not p in Leaves (dom T) or T . p <> x ) ; :: thesis: f . p = T . p
A8: p in W by A1;

now :: thesis: for p9 being Node of T
for q being Node of T9 holds
( not p = p9 ^ q or not p9 in Leaves (dom T) or not T . p9 = x or not f . p = T9 . q )

given p9 being Node of T, q being Node of T9 such that A9: p = p9 ^ q and
A10: p9 in Leaves (dom T) and
A11: T . p9 = x and
f . p = T9 . q ; :: thesis: contradiction
( p9 is_a_prefix_of p & not p9 is_a_proper_prefix_of p ) by A9, A10, TREES_1:1, TREES_1:def 5;
hence contradiction by A7, A10, A11, XBOOLE_0:def 8; :: thesis: verum

end;

hence f . p = T . p by A6, A8; :: thesis: verum

end;

let p be Node of T; :: thesis: for q being Node of T9 st p in Leaves (dom T) & T . p = x holds
f . (p ^ q) = T9 . q
let q be Node of T9; :: thesis: ( p in Leaves (dom T) & T . p = x implies f . (p ^ q) = T9 . q )
assume that
A12: p in Leaves (dom T) and
A13: T . p = x ; :: thesis: f . (p ^ q) = T9 . q
A14: p ^ q in W by A1, A12, A13;

now :: thesis: ( p ^ q is Node of T implies p = p ^ q )

assume p ^ q is Node of T ; :: thesis: p = p ^ q
then A15: not p is_a_proper_prefix_of p ^ q by A12, TREES_1:def 5;
p is_a_prefix_of p ^ q by TREES_1:1;
hence p = p ^ q by A15, XBOOLE_0:def 8; :: thesis: verum

end;

then consider p9 being Node of T, q9 being Node of T9 such that
A16: p ^ q = p9 ^ q9 and
A17: p9 in Leaves (dom T) and
T . p9 = x and
A18: f . (p ^ q) = T9 . q9 by A6, A12, A13, A14;

now :: thesis: for p, p9, q, q9 being FinSequence of NAT
for T being Tree st p ^ q = p9 ^ q9 & p in Leaves T & p9 in Leaves T holds
not p <> p9

let p, p9, q, q9 be FinSequence of NAT ; :: thesis: for T being Tree st p ^ q = p9 ^ q9 & p in Leaves T & p9 in Leaves T holds
not p <> p9
let T be Tree; :: thesis: ( p ^ q = p9 ^ q9 & p in Leaves T & p9 in Leaves T implies not p <> p9 )
assume that
A19: p ^ q = p9 ^ q9 and
A20: ( p in Leaves T & p9 in Leaves T ) and
A21: p <> p9 ; :: thesis: contradiction

now :: thesis: not len p <= len p9

assume len p <= len p9 ; :: thesis: contradiction
then ex r being FinSequence st p ^ r = p9 by A19, FINSEQ_1:47;
then p is_a_prefix_of p9 by TREES_1:1;
then p is_a_proper_prefix_of p9 by A21, XBOOLE_0:def 8;
hence contradiction by A20, TREES_1:def 5; :: thesis: verum

end;

then ex r being FinSequence st p9 ^ r = p by A19, FINSEQ_1:47;
then p9 is_a_prefix_of p by TREES_1:1;
then p9 is_a_proper_prefix_of p by A21, XBOOLE_0:def 8;
hence contradiction by A20, TREES_1:def 5; :: thesis: verum

end;

then p = p9 by A12, A16, A17;
hence f . (p ^ q) = T9 . q by A16, A18, FINSEQ_1:33; :: thesis: verum