let t, t1 be Tree; 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; ( not xi c= nu & not nu c= xi implies (t with-replacement (xi,t1)) | nu = t | nu )
assume Z0:
not xi c= nu
; ( nu c= xi or (t with-replacement (xi,t1)) | nu = t | nu )
assume Z1:
not nu c= xi
; (t with-replacement (xi,t1)) | nu = t | nu
let a be FinSequence of NAT ; TREES_2:def 1 ( ( 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 ) )
assume
a in t | nu
; 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; verum