theorem :: ZF_MODEL:10

for H being ZF-formula
for E being non empty set st H is conjunctive holds
for f being Function of VAR,E holds
( ( f in St ((the_left_argument_of H),E) & f in St ((the_right_argument_of H),E) ) iff f in St (H,E) )