ex f being Function st
( dom f = NAT & f . 0 = F₁() & ( for n being Nat holds P₁[n,f . n,f . (n + 1)] ) )

A1: for n being Nat
for x being set ex y being set st P₁[n,x,y]