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 TREES_4:sch 1();
 defpred S2[ 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 T9 st
( $1 = p ^ q & p in Leaves (dom T) & T . p = x & $2 = T9 . q ) );
A2: for z being set st z in W holds
ex y being set st S2[z,y]
proof
let z be set ; :: thesis: ( z in W implies ex y being set st S2[z,y] )
assume A3: z in W ; :: thesis: ex y being set st S2[z,y]
reconsider w = z as Element of W by A3;
A4: now
given q being Node of T, r being Node of T9 such that A5: ( 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 A5; :: thesis: verum
end;
A6: now
assume A7: 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, A7; :: thesis: ( ( not z in Leaves (dom T) or T . z <> x ) & y = T . z )
reconsider w = w as Node of T by A1, A7;
reconsider e = {} as Node of T9 by TREES_1:47;
A8: w ^ e = w by FINSEQ_1:47;
thus ( ( not z in Leaves (dom T) or T . z <> x ) & y = T . z ) by A7, A8; :: thesis: verum
end;
thus ex y being set st S2[z,y] by A4, A6; :: thesis: verum
end;
consider f being Function such that
A9: ( dom f = W & ( for z being set st z in W holds
S2[z,f . z] ) ) from CLASSES1:sch 1(A2);
 reconsider f = f as DecoratedTree by A9, 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, A9; :: 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 A10: ( not p in Leaves (dom T) or T . p <> x ) ; :: thesis: f . p = T . p
A11: p in W by A1;
A12: now
given p9 being Node of T, q being Node of T9 such that A13: p = p9 ^ q and
A14: p9 in Leaves (dom T) and
A15: T . p9 = x and
f . p = T9 . q ; :: thesis: contradiction
A16: ( p9 is_a_prefix_of p & not p9 is_a_proper_prefix_of p ) by A13, A14, TREES_1:8, TREES_1:def 8;
thus contradiction by A10, A14, A15, A16, XBOOLE_0:def 8; :: thesis: verum
end;
thus f . p = T . p by A9, A11, A12; :: 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
A17: p in Leaves (dom T) and
A18: T . p = x ; :: thesis: f . (p ^ q) = T9 . q
A19: p ^ q in W by A1, A17, A18;
A20: now
assume A21: p ^ q is Node of T ; :: thesis: p = p ^ q
A22: not p is_a_proper_prefix_of p ^ q by A17, A21, TREES_1:def 8;
A23: p is_a_prefix_of p ^ q by TREES_1:8;
thus p = p ^ q by A22, A23, XBOOLE_0:def 8; :: thesis: verum
end;
consider p9 being Node of T, q9 being Node of T9 such that
A24: p ^ q = p9 ^ q9 and
A25: p9 in Leaves (dom T) and
T . p9 = x and
A26: f . (p ^ q) = T9 . q9 by A9, A17, A18, A19, A20;
A27: now
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
A28: p ^ q = p9 ^ q9 and
A29: ( p in Leaves T & p9 in Leaves T ) and
A30: p <> p9 ; :: thesis: contradiction
A31: now
assume A32: len p <= len p9 ; :: thesis: contradiction
A33: ex r being FinSequence st p ^ r = p9 by A28, A32, FINSEQ_1:64;
A34: p is_a_prefix_of p9 by A33, TREES_1:8;
A35: p is_a_proper_prefix_of p9 by A30, A34, XBOOLE_0:def 8;
thus contradiction by A29, A35, TREES_1:def 8; :: thesis: verum
end;
A36: ex r being FinSequence st p9 ^ r = p by A28, A31, FINSEQ_1:64;
A37: p9 is_a_prefix_of p by A36, TREES_1:8;
A38: p9 is_a_proper_prefix_of p by A30, A37, XBOOLE_0:def 8;
thus contradiction by A29, A38, TREES_1:def 8; :: thesis: verum
end;
A39: p = p9 by A17, A24, A25, A27;
thus f . (p ^ q) = T9 . q by A24, A26, A39, FINSEQ_1:46; :: thesis: verum