A2: Seg (len p) = dom p by FINSEQ_1:def 3;
A3: for k being Nat st k in Seg (len p) holds
ex x being object st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg (len p) implies ex x being object st S₁[k,x] )
assume k in Seg (len p) ; :: thesis: ex x being object st S₁[k,x]
then A4: p . k in rng p by A2, FUNCT_1:def 3;
rng p is constituted-DTrees by A1;
then reconsider T = p . k as DecoratedTree by A4;
take T . {} ; :: thesis: S₁[k,T . {}]
take T ; :: thesis: ( T = p . k & T . {} = T . {} )
thus ( T = p . k & T . {} = T . {} ) ; :: thesis: verum

end;

consider q being FinSequence such that
A5: ( dom q = Seg (len p) & ( for k being Nat st k in Seg (len p) holds
S₁[k,q . k] ) ) from FINSEQ_1:sch 1(A3);
take q ; :: thesis: ( dom q = dom p & ( for i being Element of NAT st i in dom p holds
ex T being DecoratedTree st
( T = p . i & q . i = T . {} ) ) )
thus dom q = dom p by A5, FINSEQ_1:def 3; :: thesis: for i being Element of NAT st i in dom p holds
ex T being DecoratedTree st
( T = p . i & q . i = T . {} )
thus for i being Element of NAT st i in dom p holds
ex T being DecoratedTree st
( T = p . i & q . i = T . {} ) by A2, A5; :: thesis: verum