let H be ZF-formula; :: thesis: 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) )
let E be non empty set ; :: thesis: ( H is conjunctive implies 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) ) )
assume H is conjunctive ; :: thesis: 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) )
then H = (the_left_argument_of H) '&' (the_right_argument_of H) by ZF_LANG:40;
hence 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) ) by Th5; :: thesis: verum