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 T' st
( S₁[q] & p = q ^ r ) ) ) from TREES_4:sch 1();
defpred S₂[ set , set ] 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 T' st
( $1 = p ^ q & p in Leaves (dom T) & T . p = x & $2 = T' . q ) );
A2: for z being set st z in W holds
ex y being set st S₂[z,y]

proof

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

A3: now

given q being Node of T, r being Node of T' 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 T' st
( z = q ^ r & q in Leaves (dom T) & T . q = x & y = T' . r )
take y = T' . r; :: thesis: ex q being Node of T ex r being Node of T' st
( z = q ^ r & q in Leaves (dom T) & T . q = x & y = T' . r )
take q = q; :: thesis: ex r being Node of T' st
( z = q ^ r & q in Leaves (dom T) & T . q = x & y = T' . r )
take r = r; :: thesis: ( z = q ^ r & q in Leaves (dom T) & T . q = x & y = T' . r )
thus ( z = q ^ r & q in Leaves (dom T) & T . q = x & y = T' . r ) by A4; :: thesis: verum

end;

now

assume A5: for q being Node of T
for r being Node of T' 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 T' by TREES_1:47;
w ^ e = w by FINSEQ_1:47;
hence ( ( not z in Leaves (dom T) or T . z <> x ) & y = T . z ) by A5; :: thesis: verum

end;

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

end;

consider f being Function such that
A6: ( dom f = W & ( for z being set 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 T' 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 T' st p in Leaves (dom T) & T . p = x holds
f . (p ^ q) = T' . 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 T' 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 T' st p in Leaves (dom T) & T . p = x holds
f . (p ^ q) = T' . 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 T' st p in Leaves (dom T) & T . p = x holds
f . (p ^ q) = T' . 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

given p' being Node of T, q being Node of T' such that A9: ( p = p' ^ q & p' in Leaves (dom T) & T . p' = x & f . p = T' . q ) ; :: thesis: contradiction
( p' is_a_prefix_of p & not p' is_a_proper_prefix_of p ) by A9, TREES_1:8, TREES_1:def 8;
hence contradiction by A7, A9, 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 T' st p in Leaves (dom T) & T . p = x holds
f . (p ^ q) = T' . q
let q be Node of T'; :: thesis: ( p in Leaves (dom T) & T . p = x implies f . (p ^ q) = T' . q )
assume A10: ( p in Leaves (dom T) & T . p = x ) ; :: thesis: f . (p ^ q) = T' . q
then A11: p ^ q in W by A1;

now

assume p ^ q is Node of T ; :: thesis: p = p ^ q
then ( not p is_a_proper_prefix_of p ^ q & p is_a_prefix_of p ^ q ) by A10, TREES_1:8, TREES_1:def 8;
hence p = p ^ q by XBOOLE_0:def 8; :: thesis: verum

end;

then consider p' being Node of T, q' being Node of T' such that
A12: ( p ^ q = p' ^ q' & p' in Leaves (dom T) & T . p' = x & f . (p ^ q) = T' . q' ) by A6, A10, A11;

now

let p, p', q, q' be FinSequence of NAT ; :: thesis: for T being Tree st p ^ q = p' ^ q' & p in Leaves T & p' in Leaves T holds
not p <> p'
let T be Tree; :: thesis: ( p ^ q = p' ^ q' & p in Leaves T & p' in Leaves T implies not p <> p' )
assume A13: ( p ^ q = p' ^ q' & p in Leaves T & p' in Leaves T & p <> p' ) ; :: thesis: contradiction

now

assume len p <= len p' ; :: thesis: contradiction
then consider r being FinSequence such that
A14: p ^ r = p' by A13, FINSEQ_1:64;
p is_a_prefix_of p' by A14, TREES_1:8;
then p is_a_proper_prefix_of p' by A13, XBOOLE_0:def 8;
hence contradiction by A13, TREES_1:def 8; :: thesis: verum

end;

then consider r being FinSequence such that
A15: p' ^ r = p by A13, FINSEQ_1:64;
p' is_a_prefix_of p by A15, TREES_1:8;
then p' is_a_proper_prefix_of p by A13, XBOOLE_0:def 8;
hence contradiction by A13, TREES_1:def 8; :: thesis: verum

end;

then p = p' by A10, A12;
hence f . (p ^ q) = T' . q by A12, FINSEQ_1:46; :: thesis: verum