theorem Th4: :: ZF_FUND2:4

for H being ZF-formula
for M being non empty set
for v being Function of VAR,M holds Section (H,v) = { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) }