deffunc H₁( set , set ) -> set = $1;
set Y = { H₁(x,F₁()) where x is Element of F₁() : P₁[x,F₁()] } ;
A2: for y being set st y in F₁() holds
ex x being set st
( x in F₁() & P₁[x,F₁()] & y = H₁(x,F₁()) ) by A1;
F₁() c= { H₁(x,F₁()) where x is Element of F₁() : P₁[x,F₁()] } from FOMODEL0:sch 4(A2);
hence F₁() c= { x where x is Element of F₁() : P₁[x,F₁()] } ; :: thesis: verum