let p be FinSequence; :: thesis: ( p is Tree-yielding implies ( (tree p) -level 1 = { <*n*> where n is Element of NAT : n < len p } & ( for n being Element of NAT st n < len p holds
(tree p) | <*n*> = p . (n + 1) ) ) )
set T = tree p;
assume A1: p is Tree-yielding ; :: thesis: ( (tree p) -level 1 = { <*n*> where n is Element of NAT : n < len p } & ( for n being Element of NAT st n < len p holds
(tree p) | <*n*> = p . (n + 1) ) )
then A2: rng p is constituted-Trees by Def9;
thus (tree p) -level 1 = { <*n*> where n is Element of NAT : n < len p } :: thesis: for n being Element of NAT st n < len p holds
(tree p) | <*n*> = p . (n + 1)

proof

thus (tree p) -level 1 c= { <*n*> where n is Element of NAT : n < len p } :: according to XBOOLE_0:def 10 :: thesis: { <*n*> where n is Element of NAT : n < len p } c= (tree p) -level 1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (tree p) -level 1 or x in { <*n*> where n is Element of NAT : n < len p } )
assume x in (tree p) -level 1 ; :: thesis: x in { <*n*> where n is Element of NAT : n < len p }
then consider t being Element of tree p such that
A3: ( x = t & len t = 1 ) ;
A4: t = <*(t . 1)*> by A3, FINSEQ_1:57;
then consider n being Element of NAT , q being FinSequence such that
A5: ( n < len p & q in p . (n + 1) & t = <*n*> ^ q ) by A1, Def15;
t = <*n*> by A4, A5, TREES_1:6;
hence x in { <*n*> where n is Element of NAT : n < len p } by A3, A5; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { <*n*> where n is Element of NAT : n < len p } or x in (tree p) -level 1 )
assume x in { <*n*> where n is Element of NAT : n < len p } ; :: thesis: x in (tree p) -level 1
then consider n being Element of NAT such that
A6: ( x = <*n*> & n < len p ) ;
p . (n + 1) in rng p by A6, Lm4;
then p . (n + 1) is Tree by A2, Def3;
then ( {} in p . (n + 1) & <*n*> ^ {} = <*n*> & <*n*> in NAT * ) by FINSEQ_1:47, FINSEQ_1:def 11, TREES_1:47;
then reconsider t = <*n*> as Element of tree p by A1, A6, Def15;
len t = 1 by FINSEQ_1:56;
hence x in (tree p) -level 1 by A6; :: thesis: verum

end;

let n be Element of NAT ; :: thesis: ( n < len p implies (tree p) | <*n*> = p . (n + 1) )
assume A7: n < len p ; :: thesis: (tree p) | <*n*> = p . (n + 1)
then p . (n + 1) in rng p by Lm4;
then reconsider S = p . (n + 1) as Tree by A2, Def3;
( {} in S & <*n*> ^ {} = <*n*> & <*n*> in NAT * ) by FINSEQ_1:47, FINSEQ_1:def 11, TREES_1:47;
then A8: <*n*> in tree p by A1, A7, Def15;
(tree p) | <*n*> = S

proof

let r be FinSequence of NAT ; :: according to TREES_2:def 1 :: thesis: ( ( not r in (tree p) | <*n*> or r in S ) & ( not r in S or r in (tree p) | <*n*> ) )
thus ( r in (tree p) | <*n*> implies r in S ) :: thesis: ( not r in S or r in (tree p) | <*n*> )

proof

assume r in (tree p) | <*n*> ; :: thesis: r in S
then ( {} <> <*n*> & <*n*> ^ r in tree p ) by A8, TREES_1:def 9;
then consider m being Element of NAT , q being FinSequence such that
A9: ( m < len p & q in p . (m + 1) & <*n*> ^ r = <*m*> ^ q ) by A1, Def15;
( (<*n*> ^ r) . 1 = n & (<*m*> ^ q) . 1 = m ) by FINSEQ_1:58;
hence r in S by A9, FINSEQ_1:46; :: thesis: verum

end;

assume r in S ; :: thesis: r in (tree p) | <*n*>
then A10: <*n*> ^ r in tree p by A1, A7, Def15;
then <*n*> in tree p by TREES_1:46;
hence r in (tree p) | <*n*> by A10, TREES_1:def 9; :: thesis: verum

end;

hence (tree p) | <*n*> = p . (n + 1) ; :: thesis: verum