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: ( union {(St H,E)} = St H,E & union {(St H9,E)} = St H9,E ) by ZFMISC_1:31;
A2: H '&' H9 is conjunctive by ZF_LANG:16;
then A3: St (H '&' H9),E = (union {(St (the_left_argument_of (H '&' H9)),E)}) /\ (union {(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 A2, ZF_LANG:58;
then A4: ( H = the_left_argument_of (H '&' H9) & H9 = the_right_argument_of (H '&' H9) ) by ZF_LANG:47;
hence ( f in St H,E & f in St H9,E implies f in St (H '&' H9),E ) by A3, A1, 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 A3, A4, A1, XBOOLE_0:def 4; :: thesis: verum