let p be non empty Tree-yielding FinSequence; :: thesis: Leaves (tree p) = { (<*i*> ^ q) where i is Nat, q is FinSequence of NAT , d is Tree : ( q in Leaves d & i + 1 in dom p & d = p . (i + 1) ) }
set i0 = the Element of dom p;
reconsider d0 = p . the Element of dom p as Tree by TREES_3:22;
consider j being Nat such that
A0: the Element of dom p = 1 + j by NAT_1:10, FINSEQ_3:25;
the Element of dom p <= len p by FINSEQ_3:25;
then A3: ( j < len p & <*> NAT in d0 ) by A0, NAT_1:13, TREES_1:22;
A2: <*j*> ^ {} in tree p by A0, A3, TREES_3:def 15;
thus Leaves (tree p) c= { (<*i*> ^ q) where i is Nat, q is FinSequence of NAT , d is Tree : ( q in Leaves d & i + 1 in dom p & d = p . (i + 1) ) } :: according to XBOOLE_0:def 10 :: thesis: { (<*i*> ^ q) where i is Nat, q is FinSequence of NAT , d is Tree : ( q in Leaves d & i + 1 in dom p & d = p . (i + 1) ) } c= Leaves (tree p)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Leaves (tree p) or a in { (<*i*> ^ q) where i is Nat, q is FinSequence of NAT , d is Tree : ( q in Leaves d & i + 1 in dom p & d = p . (i + 1) ) } )
reconsider x = a as set by TARSKI:1;
assume A1: a in Leaves (tree p) ; :: thesis: a in { (<*i*> ^ q) where i is Nat, q is FinSequence of NAT , d is Tree : ( q in Leaves d & i + 1 in dom p & d = p . (i + 1) ) }
then reconsider x = a as Element of tree p ;

per cases ( x = {} or ex i being Nat ex q being FinSequence st
( i < len p & q in p . (i + 1) & x = <*i*> ^ q ) ) by TREES_3:def 15;

suppose x = {} ; :: thesis: a in { (<*i*> ^ q) where i is Nat, q is FinSequence of NAT , d is Tree : ( q in Leaves d & i + 1 in dom p & d = p . (i + 1) ) }

then not {} is_a_proper_prefix_of <*j*> by A1, A2, TREES_1:def 5;
hence a in { (<*i*> ^ q) where i is Nat, q is FinSequence of NAT , d is Tree : ( q in Leaves d & i + 1 in dom p & d = p . (i + 1) ) } by XBOOLE_1:61; :: thesis: verum

end;

suppose ex i being Nat ex q being FinSequence st
( i < len p & q in p . (i + 1) & x = <*i*> ^ q ) ; :: thesis: a in { (<*i*> ^ q) where i is Nat, q is FinSequence of NAT , d is Tree : ( q in Leaves d & i + 1 in dom p & d = p . (i + 1) ) }

then consider i being Nat, q being FinSequence such that
A2: ( i < len p & q in p . (i + 1) & x = <*i*> ^ q ) ;
( 1 <= i + 1 & i + 1 <= len p ) by A2, NAT_1:11, NAT_1:13;
then AB: ( i + 1 in dom p & p is Tree-yielding ) by FINSEQ_3:25;
then ( p . (i + 1) in rng p & rng p is constituted-Trees ) by FUNCT_1:def 3, TREES_3:def 9;
then reconsider p1 = p . (i + 1) as Tree ;
reconsider q0 = q as Element of p1 by A2;

now :: thesis: not q0 nin Leaves p1

assume AA: q0 nin Leaves p1 ; :: thesis: contradiction
consider r being FinSequence of NAT such that
A3: ( r in p1 & q0 is_a_proper_prefix_of r ) by AA, TREES_1:def 5;
consider w being FinSequence such that
A5: r = q ^ w by A3, XBOOLE_0:def 8, TREES_1:1;
<*i*> ^ r = (<*i*> ^ q) ^ w by A5, FINSEQ_1:32;
then ( <*i*> ^ q is_a_prefix_of <*i*> ^ r & <*i*> ^ q <> <*i*> ^ r ) by A3, FINSEQ_1:33, TREES_1:1;
then ( x is_a_proper_prefix_of <*i*> ^ r & <*i*> ^ r in tree p ) by A2, A3, XBOOLE_0:def 8, TREES_3:def 15;
hence contradiction by A1, TREES_1:def 5; :: thesis: verum

end;

hence a in { (<*i*> ^ q) where i is Nat, q is FinSequence of NAT , d is Tree : ( q in Leaves d & i + 1 in dom p & d = p . (i + 1) ) } by A2, AB; :: thesis: verum

end;

end;

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (<*i*> ^ q) where i is Nat, q is FinSequence of NAT , d is Tree : ( q in Leaves d & i + 1 in dom p & d = p . (i + 1) ) } or x in Leaves (tree p) )
assume x in { (<*i*> ^ q) where i is Nat, q is FinSequence of NAT , d is Tree : ( q in Leaves d & i + 1 in dom p & d = p . (i + 1) ) } ; :: thesis: x in Leaves (tree p)
then consider i being Nat, q being FinSequence of NAT , d being Tree such that
B1: ( x = <*i*> ^ q & q in Leaves d & i + 1 in dom p & d = p . (i + 1) ) ;
i + 1 <= len p by B1, FINSEQ_3:25;
then i < len p by NAT_1:13;
then reconsider r = x as Element of tree p by B1, TREES_3:48;
assume x nin Leaves (tree p) ; :: thesis: contradiction
then consider q0 being FinSequence of NAT such that
B4: ( q0 in tree p & r is_a_proper_prefix_of q0 ) by TREES_1:def 5;
consider w being FinSequence such that
B6: q0 = (<*i*> ^ q) ^ w by B1, B4, XBOOLE_0:def 8, TREES_1:1;
B7: q0 = <*i*> ^ (q ^ w) by B6, FINSEQ_1:32;
then B9: q ^ w is FinSequence of NAT by FINSEQ_1:36;
( q ^ w in d & q is_a_proper_prefix_of q ^ w ) by B1, B4, B7, TREES_3:48, TREES_1:49;
hence contradiction by B1, B9, TREES_1:def 5; :: thesis: verum