let D be non empty set ; :: thesis: for F being Subset of (FinTrees D)
for p being FinSequence of F st len (roots p) = 1 holds
ex x being Element of FinTrees D st
( p = <*x*> & x in F )
let F be Subset of (FinTrees D); :: thesis: for p being FinSequence of F st len (roots p) = 1 holds
ex x being Element of FinTrees D st
( p = <*x*> & x in F )
let p be FinSequence of F; :: thesis: ( len (roots p) = 1 implies ex x being Element of FinTrees D st
( p = <*x*> & x in F ) )
assume len (roots p) = 1 ; :: thesis: ex x being Element of FinTrees D st
( p = <*x*> & x in F )
then A1: dom (roots p) = Seg 1 by FINSEQ_1:def 3;
A2: dom p = dom (roots p) by TREES_3:def 18;
then A3: 1 in dom p by A1;
then reconsider x = p . 1 as Element of FinTrees D by Th2;
take x ; :: thesis: ( p = <*x*> & x in F )
thus ( p = <*x*> & x in F ) by A1, A2, A3, Th2, FINSEQ_1:def 8; :: thesis: verum