theorem Th29: :: ZF_LANG:29

for F, H being ZF-formula
for sq being FinSequence st H = F ^ sq holds
H = F