theorem Th35: :: HILBERT2:35

for p being Element of HP-WFF
for f being Element of dom (Subformulae p) holds (Subformulae p) | f = Subformulae ((Subformulae p) . f)