let x be set ; for p being non empty DTree-yielding FinSequence holds Subtrees (x -tree p) = {(x -tree p)} \/ (Subtrees (rng p))
let p be non empty DTree-yielding FinSequence; Subtrees (x -tree p) = {(x -tree p)} \/ (Subtrees (rng p))
thus
Subtrees (x -tree p) c= {(x -tree p)} \/ (Subtrees (rng p))
XBOOLE_0:def 10 {(x -tree p)} \/ (Subtrees (rng p)) c= Subtrees (x -tree p)proof
let y be
object ;
TARSKI:def 3 ( not y in Subtrees (x -tree p) or y in {(x -tree p)} \/ (Subtrees (rng p)) )
assume
y in Subtrees (x -tree p)
;
y in {(x -tree p)} \/ (Subtrees (rng p))
then consider q being
Element of
dom (x -tree p) such that A1:
y = (x -tree p) | q
;
A2:
dom (x -tree p) = tree (doms p)
by TREES_4:10;
per cases
( q = {} or ex n being Nat ex r being FinSequence st
( n < len (doms p) & r in (doms p) . (n + 1) & q = <*n*> ^ r ) )
by A2, TREES_3:def 15;
suppose
ex
n being
Nat ex
r being
FinSequence st
(
n < len (doms p) &
r in (doms p) . (n + 1) &
q = <*n*> ^ r )
;
y in {(x -tree p)} \/ (Subtrees (rng p))then consider n being
Nat,
r being
FinSequence such that A3:
(
n < len (doms p) &
r in (doms p) . (n + 1) &
q = <*n*> ^ r )
;
A4:
len (doms p) = len p
by TREES_3:38;
(
n + 1
>= 1 &
n + 1
<= len p )
by A3, A4, NAT_1:11, NAT_1:13;
then A5:
n + 1
in dom p
by FINSEQ_3:25;
then A6:
p . (n + 1) in rng p
by FUNCT_1:def 3;
then reconsider t =
p . (n + 1) as
DecoratedTree ;
reconsider r =
r as
Element of
dom t by A3, A5, FUNCT_6:22;
reconsider n =
n as
Element of
NAT by ORDINAL1:def 12;
p . (n + 1) = (x -tree p) | <*n*>
by A3, A4, TREES_4:def 4;
then
y = t | r
by A1, A3, TREES_9:3;
then
y in Subtrees (rng p)
by A6;
hence
y in {(x -tree p)} \/ (Subtrees (rng p))
by XBOOLE_0:def 3;
verum end;
end;
let z be object ; TARSKI:def 3 ( not z in {(x -tree p)} \/ (Subtrees (rng p)) or z in Subtrees (x -tree p) )
assume
z in {(x -tree p)} \/ (Subtrees (rng p))
; z in Subtrees (x -tree p)
then A7:
( z in {(x -tree p)} or z in Subtrees (rng p) )
by XBOOLE_0:def 3;
reconsider q = {} as Element of dom (x -tree p) by TREES_1:22;
per cases
( z = x -tree p or z in Subtrees (rng p) )
by A7, TARSKI:def 1;
suppose
z in Subtrees (rng p)
;
z in Subtrees (x -tree p)then consider t being
Element of
rng p,
q being
Element of
dom t such that A8:
z = t | q
;
consider y being
object such that A9:
(
y in dom p &
t = p . y )
by FUNCT_1:def 3;
reconsider y =
y as
Nat by A9;
consider n being
Nat such that A10:
y = 1
+ n
by A9, FINSEQ_3:25, NAT_1:10;
reconsider n =
n as
Element of
NAT by ORDINAL1:def 12;
y <= len p
by A9, FINSEQ_3:25;
then A11:
n < len p
by A10, NAT_1:13;
then A12:
t = (x -tree p) | <*n*>
by A9, A10, TREES_4:def 4;
A13:
tree (doms p) = dom (x -tree p)
by TREES_4:10;
(
dom t = (doms p) . y &
len (doms p) = len p )
by A9, FUNCT_6:22, TREES_3:38;
then A14:
<*n*> ^ q in dom (x -tree p)
by A10, A11, A13, TREES_3:def 15;
then
z = (x -tree p) | (<*n*> ^ q)
by A8, A12, TREES_9:3;
hence
z in Subtrees (x -tree p)
by A14;
verum end;