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