let H be ZF-formula; :: thesis: ( H is universal implies H . 1 = 4 )
assume H is universal ; :: thesis: H . 1 = 4
then consider x being Variable, H1 being ZF-formula such that
A1: H = All x,H1 by Def14;
( H = (<*4*> ^ <*x*>) ^ H1 & (<*4*> ^ <*x*>) ^ H1 = <*4*> ^ (<*x*> ^ H1) ) by A1, FINSEQ_1:45;
hence H . 1 = 4 by FINSEQ_1:58; :: thesis: verum