theorem Th6: :: CLOPBAN1:6

for X being non empty set
for Y being ComplexLinearSpace
for f being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . (f,((FuncExtMult (X,Y)) . [(- 1r),f])) = FuncZero (X,Y)