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:58;
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