theorem Th15: :: INTEGR15:15

for Z being set
for n, i being Element of NAT
for f1, f2 being PartFunc of Z,(REAL n) holds
( (proj (i,n)) * (f1 + f2) = ((proj (i,n)) * f1) + ((proj (i,n)) * f2) & (proj (i,n)) * (f1 - f2) = ((proj (i,n)) * f1) - ((proj (i,n)) * f2) )