consider A being set such that
A2: for x, y being Variable holds
( [(x '=' y),F₁(x,y)] in A & [(x 'in' y),F₂(x,y)] in A ) and
A3: [F₆(),F₇(F₆())] in A and
A4: for H being ZF-formula
for a being set st [H,a] in A holds
( ( H is being_equality implies a = F₁((Var1 H),(Var2 H)) ) & ( H is being_membership implies a = F₂((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st
( a = F₃(b) & [(the_argument_of H),b] in A ) ) & ( H is conjunctive implies ex b, c being set st
( a = F₄(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 = F₅((bound_in H),b) & [(the_scope_of H),b] in A ) ) ) by A1;
thus ( F₆() is being_equality implies F₇(F₆()) = F₁((Var1 F₆()),(Var2 F₆())) ) by A3, A4; :: thesis: ( ( F₆() is being_membership implies F₇(F₆()) = F₂((Var1 F₆()),(Var2 F₆())) ) & ( F₆() is negative implies F₇(F₆()) = F₃(F₇((the_argument_of F₆()))) ) & ( F₆() is conjunctive implies for a, b being set st a = F₇((the_left_argument_of F₆())) & b = F₇((the_right_argument_of F₆())) holds
F₇(F₆()) = F₄(a,b) ) & ( F₆() is universal implies F₇(F₆()) = F₅((bound_in F₆()),F₇((the_scope_of F₆()))) ) )
thus ( F₆() is being_membership implies F₇(F₆()) = F₂((Var1 F₆()),(Var2 F₆())) ) by A3, A4; :: thesis: ( ( F₆() is negative implies F₇(F₆()) = F₃(F₇((the_argument_of F₆()))) ) & ( F₆() is conjunctive implies for a, b being set st a = F₇((the_left_argument_of F₆())) & b = F₇((the_right_argument_of F₆())) holds
F₇(F₆()) = F₄(a,b) ) & ( F₆() is universal implies F₇(F₆()) = F₅((bound_in F₆()),F₇((the_scope_of F₆()))) ) )
thus ( F₆() is negative implies F₇(F₆()) = F₃(F₇((the_argument_of F₆()))) ) :: thesis: ( ( F₆() is conjunctive implies for a, b being set st a = F₇((the_left_argument_of F₆())) & b = F₇((the_right_argument_of F₆())) holds
F₇(F₆()) = F₄(a,b) ) & ( F₆() is universal implies F₇(F₆()) = F₅((bound_in F₆()),F₇((the_scope_of F₆()))) ) )

proof

assume F₆() is negative ; :: thesis: F₇(F₆()) = F₃(F₇((the_argument_of F₆())))
then ex b being set st
( F₇(F₆()) = F₃(b) & [(the_argument_of F₆()),b] in A ) by A3, A4;
hence F₇(F₆()) = F₃(F₇((the_argument_of F₆()))) by A1, A2, A4; :: thesis: verum

end;

thus ( F₆() is conjunctive implies for a, b being set st a = F₇((the_left_argument_of F₆())) & b = F₇((the_right_argument_of F₆())) holds
F₇(F₆()) = F₄(a,b) ) :: thesis: ( F₆() is universal implies F₇(F₆()) = F₅((bound_in F₆()),F₇((the_scope_of F₆()))) )

proof

assume F₆() is conjunctive ; :: thesis: for a, b being set st a = F₇((the_left_argument_of F₆())) & b = F₇((the_right_argument_of F₆())) holds
F₇(F₆()) = F₄(a,b)
then consider b, c being set such that
A5: F₇(F₆()) = F₄(b,c) and
A6: [(the_left_argument_of F₆()),b] in A and
A7: [(the_right_argument_of F₆()),c] in A by A3, A4;
A8: F₇((the_left_argument_of F₆())) = b by A1, A2, A4, A6;
let a1, a2 be set ; :: thesis: ( a1 = F₇((the_left_argument_of F₆())) & a2 = F₇((the_right_argument_of F₆())) implies F₇(F₆()) = F₄(a1,a2) )
assume ( a1 = F₇((the_left_argument_of F₆())) & a2 = F₇((the_right_argument_of F₆())) ) ; :: thesis: F₇(F₆()) = F₄(a1,a2)
hence F₇(F₆()) = F₄(a1,a2) by A1, A2, A4, A5, A7, A8; :: thesis: verum

end;

thus ( F₆() is universal implies F₇(F₆()) = F₅((bound_in F₆()),F₇((the_scope_of F₆()))) ) :: thesis: verum

proof

assume F₆() is universal ; :: thesis: F₇(F₆()) = F₅((bound_in F₆()),F₇((the_scope_of F₆())))
then ex b being set st
( F₇(F₆()) = F₅((bound_in F₆()),b) & [(the_scope_of F₆()),b] in A ) by A3, A4;
hence F₇(F₆()) = F₅((bound_in F₆()),F₇((the_scope_of F₆()))) by A1, A2, A4; :: thesis: verum

end;