A2: for x being set st x in F₁() holds
ex y being set st P₁[x,y]

proof

let x be set ; :: thesis: ( x in F₁() implies ex y being set st P₁[x,y] )
assume x in F₁() ; :: thesis: ex y being set st P₁[x,y]
then reconsider p = x as Element of F₁() ;
ex y being set st P₁[p,y] by A1;
hence ex y being set st P₁[x,y] ; :: thesis: verum

end;

consider f being Function such that
A5: ( dom f = F₁() & ( for x being set st x in F₁() holds
P₁[x,f . x] ) ) from CLASSES1:sch 1(A2);
reconsider T = f as DecoratedTree by A5, Def8;
take T ; :: thesis: ( dom T = F₁() & ( for p being FinSequence of NAT st p in F₁() holds
P₁[p,T . p] ) )
thus ( dom T = F₁() & ( for p being FinSequence of NAT st p in F₁() holds
P₁[p,T . p] ) ) by A5; :: thesis: verum