let Z, Z1, Z2 be Tree; :: thesis:
let z be Element of Z; :: thesis:
assume A1: Z with-replacement (z,Z1) = Z with-replacement (z,Z2) ; :: thesis:

now :: thesis:

let s be FinSequence of NAT ; :: thesis:
thus ( s in Z1 implies s in Z2 ) :: thesis:

proof

assume A2: s in Z1 ; :: thesis:

per cases ;

suppose s = {} ; :: thesis:

hence s in Z2 by TREES_1:22; :: thesis:

end;

suppose s <> {} ; :: thesis:

then A3: z is_a_proper_prefix_of z ^ s by TREES_1:10;
z ^ s in Z with-replacement (z,Z2) by A1, A2, TREES_1:def 9;
then ex w being FinSequence of NAT st
( w in Z2 & z ^ s = z ^ w ) by A3, TREES_1:def 9;
hence s in Z2 by FINSEQ_1:33; :: thesis:

end;

end;

end;

assume A4: s in Z2 ; :: thesis:

per cases ;

suppose s = {} ; :: thesis:

hence s in Z1 by TREES_1:22; :: thesis:

end;

suppose s <> {} ; :: thesis:

then A5: z is_a_proper_prefix_of z ^ s by TREES_1:10;
z ^ s in Z with-replacement (z,Z1) by A1, A4, TREES_1:def 9;
then ex w being FinSequence of NAT st
( w in Z1 & z ^ s = z ^ w ) by A5, TREES_1:def 9;
hence s in Z1 by FINSEQ_1:33; :: thesis:

end;

end;

end;

hence Z1 = Z2 by TREES_2:def 1; :: thesis: