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