A2: for x being object st x in Seg F₁() holds
ex y being object st P₁[x,y] by A1;
consider f being Function such that
A3: ( dom f = Seg F₁() & ( for x being object st x in Seg F₁() holds
P₁[x,f . x] ) ) from CLASSES1:sch 1(A2);
reconsider p = f as FinSequence by A3, Def2;
take p ; :: thesis: ( dom p = Seg F₁() & ( for k being Nat st k in Seg F₁() holds
P₁[k,p . k] ) )
thus ( dom p = Seg F₁() & ( for k being Nat st k in Seg F₁() holds
P₁[k,p . k] ) ) by A3; :: thesis: verum