defpred S₁[ ZF-formula] means P₁[F₆($1)];
deffunc H₁( ZF-formula) -> set = F₆($1);
deffunc H₂( Variable, set ) -> set = F₅($1,$2);
deffunc H₃( set , set ) -> set = F₄($1,$2);
deffunc H₄( set ) -> set = F₃($1);
deffunc H₅( Variable, Variable) -> set = F₂($1,$2);
deffunc H₆( Variable, Variable) -> set = F₁($1,$2);
A6: for H9 being ZF-formula
for a being set holds
( a = H₁(H9) iff ex A being set st
( ( for x, y being Variable holds
( [(x '=' y),H₆(x,y)] in A & [(x 'in' y),H₅(x,y)] in A ) ) & [H9,a] in A & ( for H being ZF-formula
for a being set st [H,a] in A holds
( ( H is being_equality implies a = H₆( Var1 H, Var2 H) ) & ( H is being_membership implies a = H₅( Var1 H, Var2 H) ) & ( H is negative implies ex b being set st
( a = H₄(b) & [(the_argument_of H),b] in A ) ) & ( H is conjunctive implies ex b, c being set st
( a = H₃(b,c) & [(the_left_argument_of H),b] in A & [(the_right_argument_of H),c] in A ) ) & ( H is universal implies ex b being set st
( a = H₂( bound_in H,b) & [(the_scope_of H),b] in A ) ) ) ) ) ) by A1;

A7: now :: thesis: for H being ZF-formula holds
( ( H is being_equality implies H₁(H) = H₆( Var1 H, Var2 H) ) & ( H is being_membership implies H₁(H) = H₅( Var1 H, Var2 H) ) & ( H is negative implies H₁(H) = H₄(H₁( the_argument_of H)) ) & ( H is conjunctive implies for a, b being set st a = H₁( the_left_argument_of H) & b = H₁( the_right_argument_of H) holds
H₁(H) = H₃(a,b) ) & ( H is universal implies H₁(H) = H₂( bound_in H,H₁( the_scope_of H)) ) )

let H be ZF-formula; :: thesis: ( ( H is being_equality implies H₁(H) = H₆( Var1 H, Var2 H) ) & ( H is being_membership implies H₁(H) = H₅( Var1 H, Var2 H) ) & ( H is negative implies H₁(H) = H₄(H₁( the_argument_of H)) ) & ( H is conjunctive implies for a, b being set st a = H₁( the_left_argument_of H) & b = H₁( the_right_argument_of H) holds
H₁(H) = H₃(a,b) ) & ( H is universal implies H₁(H) = H₂( bound_in H,H₁( the_scope_of H)) ) )
thus ( ( H is being_equality implies H₁(H) = H₆( Var1 H, Var2 H) ) & ( H is being_membership implies H₁(H) = H₅( Var1 H, Var2 H) ) & ( H is negative implies H₁(H) = H₄(H₁( the_argument_of H)) ) & ( H is conjunctive implies for a, b being set st a = H₁( the_left_argument_of H) & b = H₁( the_right_argument_of H) holds
H₁(H) = H₃(a,b) ) & ( H is universal implies H₁(H) = H₂( bound_in H,H₁( the_scope_of H)) ) ) from ZF_MODEL:sch 3(A6); :: thesis: verum

end;

A8: for H being ZF-formula st H is negative & S₁[ the_argument_of H] holds
S₁[H]

proof

let H be ZF-formula; :: thesis: ( H is negative & S₁[ the_argument_of H] implies S₁[H] )
assume H is negative ; :: thesis: ( not S₁[ the_argument_of H] or S₁[H] )
then F₆(H) = F₃(F₆((the_argument_of H))) by A7;
hence ( not S₁[ the_argument_of H] or S₁[H] ) by A3; :: thesis: verum

end;

A9: for H being ZF-formula st H is universal & S₁[ the_scope_of H] holds
S₁[H]

proof

let H be ZF-formula; :: thesis: ( H is universal & S₁[ the_scope_of H] implies S₁[H] )
assume H is universal ; :: thesis: ( not S₁[ the_scope_of H] or S₁[H] )
then F₆(H) = F₅((bound_in H),F₆((the_scope_of H))) by A7;
hence ( not S₁[ the_scope_of H] or S₁[H] ) by A5; :: thesis: verum

end;

A10: for H being ZF-formula st H is conjunctive & S₁[ the_left_argument_of H] & S₁[ the_right_argument_of H] holds
S₁[H]

proof

let H be ZF-formula; :: thesis: ( H is conjunctive & S₁[ the_left_argument_of H] & S₁[ the_right_argument_of H] implies S₁[H] )
assume H is conjunctive ; :: thesis: ( not S₁[ the_left_argument_of H] or not S₁[ the_right_argument_of H] or S₁[H] )
then F₆(H) = F₄(F₆((the_left_argument_of H)),F₆((the_right_argument_of H))) by A7;
hence ( not S₁[ the_left_argument_of H] or not S₁[ the_right_argument_of H] or S₁[H] ) by A4; :: thesis: verum

end;

A11: for H being ZF-formula st H is atomic holds
S₁[H]

proof

let H be ZF-formula; :: thesis: ( H is atomic implies S₁[H] )
assume ( H is being_equality or H is being_membership ) ; :: according to ZF_LANG:def 15 :: thesis: S₁[H]
then ( F₆(H) = F₁((Var1 H),(Var2 H)) or F₆(H) = F₂((Var1 H),(Var2 H)) ) by A7;
hence S₁[H] by A2; :: thesis: verum

end;

for H being ZF-formula holds S₁[H] from ZF_LANG:sch 1(A11, A8, A10, A9);
hence P₁[F₆(F₇())] ; :: thesis: verum