{ x where x is Element of F₂() : ex w being Element of F₁() st
( P₁[w,x] & w in F₃() ) } is finite

A1: F₃() is finite and
A2: for w being Element of F₁()
for x, y being Element of F₂() st P₁[w,x] & P₁[w,y] holds
x = y