let Z1, Z2 be Tree; :: thesis:
let p be FinSequence of NAT ; :: thesis:
assume A1: p in Z1 ; :: thesis:
set Z = Z1 with-replacement (p,Z2);
let v be Element of Z1 with-replacement (p,Z2); :: thesis:
let w be Element of Z1; :: thesis:
assume that
A2: v = w and
A3: w is_a_proper_prefix_of p ; :: thesis:
w is_a_prefix_of p by A3;
then consider r being FinSequence such that
A4: p = w ^ r by TREES_1:1;

let n be Nat; :: thesis:
assume A5: n in dom r ; :: thesis:
then (len w) + n in dom p by A4, FINSEQ_1:28;
then A6: p . ((len w) + n) in rng p by FUNCT_1:def 3;
p . ((len w) + n) = r . n by A4, A5, FINSEQ_1:def 7;
hence r . n in NAT by A6; :: thesis:

end;

then reconsider r = r as FinSequence of NAT by FINSEQ_2:12;
A7: r <> {} by A3, A4, FINSEQ_1:34;

let x be object ; :: thesis:
thus ( x in succ v implies x in succ w ) :: thesis:

assume x in succ v ; :: thesis:
then x in { (v ^ <*n*>) where n is Nat : v ^ <*n*> in Z1 with-replacement (p,Z2) } by TREES_2:def 5;
then consider n being Nat such that
A8: x = v ^ <*n*> and
A9: v ^ <*n*> in Z1 with-replacement (p,Z2) ;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
x = v ^ <*n*> by A8;
then reconsider x9 = x as FinSequence of NAT ;

per cases by A1, A8, A9, TREES_1:def 9;

suppose ( x9 in Z1 & not p is_a_proper_prefix_of x9 ) ; :: thesis:

then x in { (w ^ <*m*>) where m is Nat : w ^ <*m*> in Z1 } by A2, A8;
hence x in succ w by TREES_2:def 5; :: thesis:

end;

suppose ex r being FinSequence of NAT st
( r in Z2 & x9 = p ^ r ) ; :: thesis:

then consider s being FinSequence of NAT such that
s in Z2 and
A10: v ^ <*n*> = p ^ s by A8;
w ^ <*n*> = w ^ (r ^ s) by A2, A4, A10, FINSEQ_1:32;
then A11: <*n*> = r ^ s by FINSEQ_1:33;
s = {}

assume not s = {} ; :: thesis:
then len s > 0 by NAT_1:3;
then A12: 0 + 1 <= len s by NAT_1:13;
len r > 0 by A7, NAT_1:3;
then 0 + 1 <= len r by NAT_1:13;
then 1 + 1 <= (len r) + (len s) by A12, XREAL_1:7;
then 2 <= len <*n*> by A11, FINSEQ_1:22;
then 2 <= 1 by FINSEQ_1:39;
hence contradiction ; :: thesis:

end;

then <*n*> = r by A11, FINSEQ_1:34;
then x in { (w ^ <*m*>) where m is Nat : w ^ <*m*> in Z1 } by A1, A2, A4, A8;
hence x in succ w by TREES_2:def 5; :: thesis:

end;

end;

end;

hence x in succ w ; :: thesis:

end;

assume x in succ w ; :: thesis:
then x in { (w ^ <*n*>) where n is Nat : w ^ <*n*> in Z1 } by TREES_2:def 5;
then consider n being Nat such that
A13: x = w ^ <*n*> and
A14: w ^ <*n*> in Z1 ;
reconsider n = n as Element of NAT by ORDINAL1:def 12;

assume A15: not v ^ <*n*> in Z1 with-replacement (p,Z2) ; :: thesis:

per cases by A1, A15, TREES_1:def 9;

suppose not v ^ <*n*> in Z1 ; :: thesis:

hence contradiction by A2, A14; :: thesis:

end;

suppose p is_a_proper_prefix_of v ^ <*n*> ; :: thesis:

then r is_a_proper_prefix_of <*n*> by A2, A4, TREES_1:49;
then r in ProperPrefixes <*n*> by TREES_1:12;
then r in {{}} by TREES_1:16;
hence contradiction by A7, TARSKI:def 1; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis:

end;

then x in { (v ^ <*m*>) where m is Nat : v ^ <*m*> in Z1 with-replacement (p,Z2) } by A2, A13;
hence x in succ v by TREES_2:def 5; :: thesis:

end;

hence succ v = succ w by TARSKI:2; :: thesis: