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

A1: ( F₂() in F₁() & P₁[F₂()] ) and
A2: for x being object st x in F₁() & P₁[x] holds
ex y being object st
( y in F₁() & P₂[x,y] & P₁[y] )