let X be non empty set ; :: thesis: 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)
let Y be ComplexLinearSpace; :: thesis: for f being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . (f,((FuncExtMult (X,Y)) . [(- 1r),f])) = FuncZero (X,Y)
let f be Element of Funcs (X, the carrier of Y); :: thesis: (FuncAdd (X,Y)) . (f,((FuncExtMult (X,Y)) . [(- 1r),f])) = FuncZero (X,Y)
reconsider mj = - 1r as Element of COMPLEX by XCMPLX_0:def 2;
now :: thesis: for x being Element of X holds ((FuncAdd (X,Y)) . (f,((FuncExtMult (X,Y)) . [mj,f]))) . x = (FuncZero (X,Y)) . x
let x be Element of X; :: thesis: ((FuncAdd (X,Y)) . (f,((FuncExtMult (X,Y)) . [mj,f]))) . x = (FuncZero (X,Y)) . x
set y = f . x;
thus ((FuncAdd (X,Y)) . (f,((FuncExtMult (X,Y)) . [mj,f]))) . x = (f . x) + (((FuncExtMult (X,Y)) . [mj,f]) . x) by LOPBAN_1:1
.= (f . x) + ((- 1r) * (f . x)) by Th2
.= (f . x) + (- (f . x)) by CLVECT_1:3
.= 0. Y by RLVECT_1:5
.= (FuncZero (X,Y)) . x by Th1 ; :: thesis: verum
end;
then (FuncAdd (X,Y)) . (f,((FuncExtMult (X,Y)) . [mj,f])) = FuncZero (X,Y) by FUNCT_2:63;
hence (FuncAdd (X,Y)) . (f,((FuncExtMult (X,Y)) . [(- 1r),f])) = FuncZero (X,Y) ; :: thesis: verum