consider A being set such that
A2: for x, y being Variable holds
( [(x '=' y),F1(x,y)] in A & [(x 'in' y),F2(x,y)] in A ) and
A3: [F6(),F7(F6())] 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 = F1((Var1 H),(Var2 H)) ) & ( H is being_membership implies a = F2((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st
( a = F3(b) & [(the_argument_of H),b] in A ) ) & ( H is conjunctive implies ex b, c being set st
( a = F4(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 = F5((bound_in H),b) & [(the_scope_of H),b] in A ) ) ) by A1;
thus ( F6() is being_equality implies F7(F6()) = F1((Var1 F6()),(Var2 F6())) ) by A3, A4; :: thesis: ( ( F6() is being_membership implies F7(F6()) = F2((Var1 F6()),(Var2 F6())) ) & ( F6() is negative implies F7(F6()) = F3(F7((the_argument_of F6()))) ) & ( F6() is conjunctive implies for a, b being set st a = F7((the_left_argument_of F6())) & b = F7((the_right_argument_of F6())) holds
F7(F6()) = F4(a,b) ) & ( F6() is universal implies F7(F6()) = F5((bound_in F6()),F7((the_scope_of F6()))) ) )
thus ( F6() is being_membership implies F7(F6()) = F2((Var1 F6()),(Var2 F6())) ) by A3, A4; :: thesis: ( ( F6() is negative implies F7(F6()) = F3(F7((the_argument_of F6()))) ) & ( F6() is conjunctive implies for a, b being set st a = F7((the_left_argument_of F6())) & b = F7((the_right_argument_of F6())) holds
F7(F6()) = F4(a,b) ) & ( F6() is universal implies F7(F6()) = F5((bound_in F6()),F7((the_scope_of F6()))) ) )
thus ( F6() is negative implies F7(F6()) = F3(F7((the_argument_of F6()))) ) :: thesis: ( ( F6() is conjunctive implies for a, b being set st a = F7((the_left_argument_of F6())) & b = F7((the_right_argument_of F6())) holds
F7(F6()) = F4(a,b) ) & ( F6() is universal implies F7(F6()) = F5((bound_in F6()),F7((the_scope_of F6()))) ) )
proof
assume F6() is negative ; :: thesis: F7(F6()) = F3(F7((the_argument_of F6())))
then ex b being set st
( F7(F6()) = F3(b) & [(the_argument_of F6()),b] in A ) by A3, A4;
hence F7(F6()) = F3(F7((the_argument_of F6()))) by A1, A2, A4; :: thesis: verum
end;
thus ( F6() is conjunctive implies for a, b being set st a = F7((the_left_argument_of F6())) & b = F7((the_right_argument_of F6())) holds
F7(F6()) = F4(a,b) ) :: thesis: ( F6() is universal implies F7(F6()) = F5((bound_in F6()),F7((the_scope_of F6()))) )
proof
assume F6() is conjunctive ; :: thesis: for a, b being set st a = F7((the_left_argument_of F6())) & b = F7((the_right_argument_of F6())) holds
F7(F6()) = F4(a,b)
then consider b, c being set such that
A5: F7(F6()) = F4(b,c) and
A6: [(the_left_argument_of F6()),b] in A and
A7: [(the_right_argument_of F6()),c] in A by A3, A4;
A8: F7((the_left_argument_of F6())) = b by A1, A2, A4, A6;
let a1, a2 be set ; :: thesis: ( a1 = F7((the_left_argument_of F6())) & a2 = F7((the_right_argument_of F6())) implies F7(F6()) = F4(a1,a2) )
assume ( a1 = F7((the_left_argument_of F6())) & a2 = F7((the_right_argument_of F6())) ) ; :: thesis: F7(F6()) = F4(a1,a2)
hence F7(F6()) = F4(a1,a2) by A1, A2, A4, A5, A7, A8; :: thesis: verum
end;
thus ( F6() is universal implies F7(F6()) = F5((bound_in F6()),F7((the_scope_of F6()))) ) :: thesis: verum
proof
assume F6() is universal ; :: thesis: F7(F6()) = F5((bound_in F6()),F7((the_scope_of F6())))
then ex b being set st
( F7(F6()) = F5((bound_in F6()),b) & [(the_scope_of F6()),b] in A ) by A3, A4;
hence F7(F6()) = F5((bound_in F6()),F7((the_scope_of F6()))) by A1, A2, A4; :: thesis: verum
end;