let X be 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)
let Y be 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 f be Element of Funcs (X, the carrier of Y); (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 for x being Element of X holds ((FuncAdd (X,Y)) . (f,((FuncExtMult (X,Y)) . [mj,f]))) . x = (FuncZero (X,Y)) . xlet x be
Element of
X;
((FuncAdd (X,Y)) . (f,((FuncExtMult (X,Y)) . [mj,f]))) . x = (FuncZero (X,Y)) . xset 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
;
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)
; verum