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

now :: thesis: for s being FinSequence of NAT holds
( ( s in Z1 implies s in Z2 ) & ( s in Z2 implies s in Z1 ) )

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

proof

assume A2: s in Z1 ; :: thesis: s in Z2

per cases ( s = {} or s <> {} ) ;

suppose s = {} ; :: thesis: s in Z2

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

end;

suppose s <> {} ; :: thesis: s in Z2

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: verum

end;

end;

end;

assume A4: s in Z2 ; :: thesis: b₁ in Z1

per cases ( s = {} or s <> {} ) ;

suppose s = {} ; :: thesis: b₁ in Z1

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

end;

suppose s <> {} ; :: thesis: b₁ in Z1

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: verum

end;

end;

end;

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