A3: P₁[ <*> the carrier of F₁()] by A1;
thus for p being FinSequence of the carrier of F₁() holds P₁[p] from FINSEQ_2:sch 2(A3, A2); :: thesis: verum