let F, G be ZF-formula; :: thesis: (F '&' G) . 1 = 3
thus (F '&' G) . 1 = (<*3*> ^ (F ^ G)) . 1 by FINSEQ_1:32
.= 3 by FINSEQ_1:41 ; :: thesis: verum