let W be Tree; for p being FinSequence of NAT st p in W holds
W = W with-replacement (p,(W | p))
let p be FinSequence of NAT ; ( p in W implies W = W with-replacement (p,(W | p)) )
assume A1:
p in W
; W = W with-replacement (p,(W | p))
now for q being FinSequence of NAT holds
( ( q in W implies q in W with-replacement (p,(W | p)) ) & ( q in W with-replacement (p,(W | p)) implies q in W ) )let q be
FinSequence of
NAT ;
( ( q in W implies q in W with-replacement (p,(W | p)) ) & ( q in W with-replacement (p,(W | p)) implies q in W ) )thus
(
q in W implies
q in W with-replacement (
p,
(W | p)) )
( q in W with-replacement (p,(W | p)) implies q in W )assume that A4:
q in W with-replacement (
p,
(W | p))
and A5:
not
q in W
;
contradiction
ex
r being
FinSequence of
NAT st
(
r in W | p &
q = p ^ r )
by A1, A4, A5, TREES_1:def 9;
hence
contradiction
by A1, A5, TREES_1:def 6;
verum end;
hence
W = W with-replacement (p,(W | p))
; verum