let x be Variable; :: thesis: for H being ZF-formula holds (All (x,H)) . 1 = 4
let H be ZF-formula; :: thesis: (All (x,H)) . 1 = 4
thus (All (x,H)) . 1 = (<*4*> ^ (<*x*> ^ H)) . 1 by FINSEQ_1:32
.= 4 by FINSEQ_1:41 ; :: thesis: verum