theorem Th40: :: ORDEQ_01:40

for n being non zero Element of NAT
for f being PartFunc of REAL,(REAL-NS n)
for X being set st ( for i being Nat st 1 <= i & i <= n holds
((proj (i,n)) * f) | X is constant ) holds
f | X is constant