let t, t1 be Tree; :: thesis: for xi, nu being Element of t st not xi c= nu & not nu c= xi holds
(t with-replacement (xi,t1)) | nu = t | nu
let xi, nu be Element of t; :: thesis: ( not xi c= nu & not nu c= xi implies (t with-replacement (xi,t1)) | nu = t | nu )
assume Z0: not xi c= nu ; :: thesis: ( nu c= xi or (t with-replacement (xi,t1)) | nu = t | nu )
assume Z1: not nu c= xi ; :: thesis: (t with-replacement (xi,t1)) | nu = t | nu
let a be FinSequence of NAT ; :: according to TREES_2:def 1 :: thesis: ( ( not a in (t with-replacement (xi,t1)) | nu or a in t | nu ) & ( not a in t | nu or a in (t with-replacement (xi,t1)) | nu ) )

hereby :: thesis: ( not a in t | nu or a in (t with-replacement (xi,t1)) | nu )

assume a in (t with-replacement (xi,t1)) | nu ; :: thesis: a in t | nu
then reconsider b = a as Element of (t with-replacement (xi,t1)) | nu ;
not xi c< nu by Z0, XBOOLE_0:def 8;
then nu in t with-replacement (xi,t1) by TREES_1:def 9;
then nu ^ b in t with-replacement (xi,t1) by TREES_1:def 6;

per cases then ( ( nu ^ b in t & not xi c< nu ^ b ) or ex r being FinSequence of NAT st
( r in t1 & nu ^ b = xi ^ r ) ) by TREES_1:def 9;

suppose ( nu ^ b in t & not xi c< nu ^ b ) ; :: thesis: a in t | nu

hence a in t | nu by TREES_1:def 6; :: thesis: verum

end;

suppose ex r being FinSequence of NAT st
( r in t1 & nu ^ b = xi ^ r ) ; :: thesis: a in t | nu

then consider r being FinSequence of NAT such that
B1: ( r in t1 & nu ^ b = xi ^ r ) ;
( nu c= xi ^ r & xi c= nu ^ b ) by B1, Lem8;
hence a in t | nu by Z0, Z1, Lem8B; :: thesis: verum

end;

end;

end;

assume a in t | nu ; :: thesis: a in (t with-replacement (xi,t1)) | nu
then A2: nu ^ a in t by TREES_1:def 6;
not xi c< nu ^ a by Z0, Z1, Lem8B, XBOOLE_0:def 8;
then A3: nu ^ a in t with-replacement (xi,t1) by A2, TREES_1:def 9;
not xi c< nu by Z0, XBOOLE_0:def 8;
then nu in t with-replacement (xi,t1) by TREES_1:def 9;
hence a in (t with-replacement (xi,t1)) | nu by A3, TREES_1:def 6; :: thesis: verum