:: deftheorem defines All ZF_LANG:def 7 :
for x being Variable
for p being FinSequence of NAT holds All (x,p) = (<*4*> ^ <*x*>) ^ p;