let a be set ; :: thesis: for w being DTree-yielding FinSequence holds dom (a -tree w) = {{}} \/ (union { (<*i*> ^^ (dom (w . (i + 1)))) where i is Nat : i < len w } )
let w be DTree-yielding FinSequence; :: thesis: dom (a -tree w) = {{}} \/ (union { (<*i*> ^^ (dom (w . (i + 1)))) where i is Nat : i < len w } )
set A = { (<*i*> ^^ (dom (w . (i + 1)))) where i is Nat : i < len w } ;
thus dom (a -tree w) c= {{}} \/ (union { (<*i*> ^^ (dom (w . (i + 1)))) where i is Nat : i < len w } ) :: according to XBOOLE_0:def 10 :: thesis: {{}} \/ (union { (<*i*> ^^ (dom (w . (i + 1)))) where i is Nat : i < len w } ) c= dom (a -tree w)

proof

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in dom (a -tree w) or b in {{}} \/ (union { (<*i*> ^^ (dom (w . (i + 1)))) where i is Nat : i < len w } ) )
reconsider x = b as set by TARSKI:1;
assume b in dom (a -tree w) ; :: thesis: b in {{}} \/ (union { (<*i*> ^^ (dom (w . (i + 1)))) where i is Nat : i < len w } )

per cases then ( x = {} or ex i being Nat ex T being DecoratedTree ex q being Node of T st
( i < len w & T = w . (i + 1) & x = <*i*> ^ q ) ) by TREES_4:11;

suppose x = {} ; :: thesis: b in {{}} \/ (union { (<*i*> ^^ (dom (w . (i + 1)))) where i is Nat : i < len w } )

then x in {{}} by TARSKI:def 1;
hence b in {{}} \/ (union { (<*i*> ^^ (dom (w . (i + 1)))) where i is Nat : i < len w } ) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose ex i being Nat ex T being DecoratedTree ex q being Node of T st
( i < len w & T = w . (i + 1) & x = <*i*> ^ q ) ; :: thesis: b in {{}} \/ (union { (<*i*> ^^ (dom (w . (i + 1)))) where i is Nat : i < len w } )

then consider i being Nat, T being DecoratedTree, q being Node of T such that
A1: ( i < len w & T = w . (i + 1) & x = <*i*> ^ q ) ;
( x in <*i*> ^^ (dom T) & <*i*> ^^ (dom T) in { (<*i*> ^^ (dom (w . (i + 1)))) where i is Nat : i < len w } ) by A1;
then x in union { (<*i*> ^^ (dom (w . (i + 1)))) where i is Nat : i < len w } by TARSKI:def 4;
hence b in {{}} \/ (union { (<*i*> ^^ (dom (w . (i + 1)))) where i is Nat : i < len w } ) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in {{}} \/ (union { (<*i*> ^^ (dom (w . (i + 1)))) where i is Nat : i < len w } ) or b in dom (a -tree w) )
reconsider x = b as set by TARSKI:1;
assume b in {{}} \/ (union { (<*i*> ^^ (dom (w . (i + 1)))) where i is Nat : i < len w } ) ; :: thesis: b in dom (a -tree w)

per cases then ( x in {{}} or x in union { (<*i*> ^^ (dom (w . (i + 1)))) where i is Nat : i < len w } ) by XBOOLE_0:def 3;

suppose x in {{}} ; :: thesis: b in dom (a -tree w)

then x = {} ;
hence b in dom (a -tree w) by TREES_4:11; :: thesis: verum

end;

suppose x in union { (<*i*> ^^ (dom (w . (i + 1)))) where i is Nat : i < len w } ; :: thesis: b in dom (a -tree w)

then consider I being set such that
A2: ( x in I & I in { (<*i*> ^^ (dom (w . (i + 1)))) where i is Nat : i < len w } ) by TARSKI:def 4;
consider i being Nat such that
A3: ( I = <*i*> ^^ (dom (w . (i + 1))) & i < len w ) by A2;
consider q being Element of dom (w . (i + 1)) such that
A4: ( x = <*i*> ^ q & q in dom (w . (i + 1)) ) by A2, A3;
( 1 <= i + 1 & i + 1 <= len w ) by A3, NAT_1:11, NAT_1:13;
then i + 1 in dom w by FINSEQ_3:25;
then w . (i + 1) in rng w by FUNCT_1:def 3;
then reconsider T = w . (i + 1) as DecoratedTree ;
q in dom T ;
hence b in dom (a -tree w) by A3, A4, TREES_4:11; :: thesis: verum

end;

end;