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