defpred S1[ 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
( S1[q] & p = q ^ r ) ) ) from defpred S2[ 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 S2[z,y]
proof
let z be object ; :: thesis: ( z in W implies ex y being object st S2[z,y] )
assume z in W ; :: thesis: ex y being object st S2[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 S2[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
S2[z,f . z] ) ) from reconsider f = f as DecoratedTree by ;
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 ;
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 ;
p is_a_prefix_of p ^ q by TREES_1:1;
hence p = p ^ q by ; :: 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 p9end;
then ex r being FinSequence st p9 ^ r = p by ;
then p9 is_a_prefix_of p by TREES_1:1;
then p9 is_a_proper_prefix_of p by ;
hence contradiction by A20, TREES_1:def 5; :: thesis: verum
end;
then p = p9 by ;
hence f . (p ^ q) = T9 . q by ; :: thesis: verum