let H be ZF-formula; :: thesis: ( H is conjunctive implies H . 1 = 3 )
assume H is conjunctive ; :: thesis: H . 1 = 3
then consider F, G being ZF-formula such that
A1: H = F '&' G ;
(<*3*> ^ F) ^ G = <*3*> ^ (F ^ G) by FINSEQ_1:32;
hence H . 1 = 3 by A1, FINSEQ_1:41; :: thesis: verum