let E be non empty set ; :: thesis: for H, H9 being ZF-formula
for f being Function of VAR,E holds
( ( f in St (H,E) & f in St (H9,E) ) iff f in St ((H '&' H9),E) )
let H, H9 be ZF-formula; :: thesis: for f being Function of VAR,E holds
( ( f in St (H,E) & f in St (H9,E) ) iff f in St ((H '&' H9),E) )
let f be Function of VAR,E; :: thesis: ( ( f in St (H,E) & f in St (H9,E) ) iff f in St ((H '&' H9),E) )
A1: H '&' H9 is conjunctive ;
then A2: St ((H '&' H9),E) = (St ((the_left_argument_of (H '&' H9)),E)) /\ (St ((the_right_argument_of (H '&' H9)),E)) by Lm3;
H '&' H9 = (the_left_argument_of (H '&' H9)) '&' (the_right_argument_of (H '&' H9)) by A1, ZF_LANG:40;
then A3: ( H = the_left_argument_of (H '&' H9) & H9 = the_right_argument_of (H '&' H9) ) by ZF_LANG:30;
hence ( f in St (H,E) & f in St (H9,E) implies f in St ((H '&' H9),E) ) by A2, XBOOLE_0:def 4; :: thesis: ( f in St ((H '&' H9),E) implies ( f in St (H,E) & f in St (H9,E) ) )
assume f in St ((H '&' H9),E) ; :: thesis: ( f in St (H,E) & f in St (H9,E) )
hence ( f in St (H,E) & f in St (H9,E) ) by A2, A3, XBOOLE_0:def 4; :: thesis: verum