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 A3: x in F₁() ; :: thesis: ex y being set st P₁[x,y]
F₁() = { i where i is Element of NAT : i < F₁() } by AXIOMS:4;
then ex i being Element of NAT st
( i = x & i < F₁() ) by A3;
hence ex y being set st P₁[x,y] by A1, A3; :: thesis: verum

end;

consider f being Function such that
A4: ( dom f = F₁() & ( for x being set st x in F₁() holds
P₁[x,f . x] ) ) from CLASSES1:sch 1(A2);
reconsider p = f as XFinSequence by A4, Th7;
take p ; :: thesis: ( dom p = F₁() & ( for k being Nat st k in F₁() holds
P₁[k,p . k] ) )
thus ( dom p = F₁() & ( for k being Nat st k in F₁() holds
P₁[k,p . k] ) ) by A4; :: thesis: verum