for F being Function st rng F is finite holds
P₁[F]

A1: P₁[ {} ] and
A2: for F being Function st ( for x being set st x in rng F & P₂[x,F] holds
P₁[F | ((dom F) \ (F " {x}))] ) holds
P₁[F]