let t, t1 be Tree; :: thesis: for xi being Element of t holds (t with-replacement (xi,t1)) | xi = t1
let xi be Element of t; :: thesis: (t with-replacement (xi,t1)) | xi = t1
let p be FinSequence of NAT ; :: according to TREES_2:def 1 :: thesis: ( ( not p in (t with-replacement (xi,t1)) | xi or p in t1 ) & ( not p in t1 or p in (t with-replacement (xi,t1)) | xi ) )
A1: xi in t with-replacement (xi,t1) by TREES_1:def 9;

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

assume p in (t with-replacement (xi,t1)) | xi ; :: thesis: p in t1
then xi ^ p in t with-replacement (xi,t1) by A1, TREES_1:def 6;
hence p in t1 by Th01; :: thesis: verum

end;

assume p in t1 ; :: thesis: p in (t with-replacement (xi,t1)) | xi
then xi ^ p in t with-replacement (xi,t1) by TREES_1:def 9;
hence p in (t with-replacement (xi,t1)) | xi by A1, TREES_1:def 6; :: thesis: verum