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: not p,w are_c=-comparable ; :: thesis:
A4: not p is_a_prefix_of w by A3;

now :: thesis:

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

proof

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
A5: x = v ^ <*n*> and
A6: v ^ <*n*> in Z1 with-replacement (p,Z2) ;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
x = v ^ <*n*> by A5;
then reconsider x9 = x as FinSequence of NAT ;
v ^ <*n*> in Z1

proof

assume A7: not v ^ <*n*> in Z1 ; :: thesis:
then ex t being FinSequence of NAT st
( t in Z2 & x9 = p ^ t ) by A1, A5, A6, TREES_1:def 9;
then A8: p is_a_prefix_of v ^ <*n*> by A5, TREES_1:1;

per cases by A8;

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

hence contradiction by A2, A4, TREES_1:9; :: thesis:

end;

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

hence contradiction by A1, A7; :: thesis:

end;

end;

end;

then x in { (w ^ <*m*>) where m is Nat : w ^ <*m*> in Z1 } by A2, A5;
hence x in succ w by TREES_2:def 5; :: 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
A9: x = w ^ <*n*> and
A10: w ^ <*n*> in Z1 ;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
not p is_a_proper_prefix_of w ^ <*n*> by A4, TREES_1:9;
then v ^ <*n*> in Z1 with-replacement (p,Z2) by A1, A2, A10, TREES_1:def 9;
then x in { (v ^ <*m*>) where m is Nat : v ^ <*m*> in Z1 with-replacement (p,Z2) } by A2, A9;
hence x in succ v by TREES_2:def 5; :: thesis:

end;

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