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:45
.= 4 by FINSEQ_1:58 ; :: thesis: verum