let p be FinSequence; :: thesis: ( p is Tree-yielding implies ( (tree p) -level 1 = { <*n*> where n is 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 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 ;
thus (tree p) -level 1 = { <*n*> where n is 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 Nat : n < len p } :: according to XBOOLE_0:def 10 :: thesis: { <*n*> where n is Nat : n < len p } c= (tree p) -level 1

proof

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

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { <*n*> where n is Nat : n < len p } or x in (tree p) -level 1 )
assume x in { <*n*> where n is Nat : n < len p } ; :: thesis: x in (tree p) -level 1
then consider n being Nat such that
A8: x = <*n*> and
A9: n < len p ;
p . (n + 1) in rng p by A9, Lm3;
then A10: {} in p . (n + 1) by A2, TREES_1:22;
<*n*> ^ {} = <*n*> by FINSEQ_1:34;
then reconsider t = <*n*> as Element of tree p by A1, A9, A10, Def15;
len t = 1 by FINSEQ_1:39;
hence x in (tree p) -level 1 by A8; :: thesis: verum

end;

let n be Element of NAT ; :: thesis: ( n < len p implies (tree p) | <*n*> = p . (n + 1) )
assume A11: n < len p ; :: thesis: (tree p) | <*n*> = p . (n + 1)
then p . (n + 1) in rng p by Lm3;
then reconsider S = p . (n + 1) as Tree by A2;
A12: {} in S by TREES_1:22;
<*n*> ^ {} = <*n*> by FINSEQ_1:34;
then A13: <*n*> in tree p by A1, A11, A12, 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*> ^ r in tree p by A13, TREES_1:def 6;
then consider m being Nat, q being FinSequence such that
m < len p and
A14: q in p . (m + 1) and
A15: <*n*> ^ r = <*m*> ^ q by A1, Def15;
A16: (<*n*> ^ r) . 1 = n by FINSEQ_1:41;
(<*m*> ^ q) . 1 = m by FINSEQ_1:41;
hence r in S by A14, A15, A16, FINSEQ_1:33; :: thesis: verum

end;

assume r in S ; :: thesis: r in (tree p) | <*n*>
then A17: <*n*> ^ r in tree p by A1, A11, Def15;
then <*n*> in tree p by TREES_1:21;
hence r in (tree p) | <*n*> by A17, TREES_1:def 6; :: thesis: verum

end;

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