theorem Th28: :: ORDEQ_01:28

for n, i being Nat
for f being PartFunc of REAL,(REAL n)
for A being Subset of REAL holds (proj (i,n)) * (f | A) = ((proj (i,n)) * f) | A