let X be non empty set ; for Y being RealLinearSpace
for f being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . (f,((FuncExtMult (X,Y)) . [(- 1),f])) = FuncZero (X,Y)
let Y be RealLinearSpace; for f being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . (f,((FuncExtMult (X,Y)) . [(- 1),f])) = FuncZero (X,Y)
let f be Element of Funcs (X, the carrier of Y); (FuncAdd (X,Y)) . (f,((FuncExtMult (X,Y)) . [(- 1),f])) = FuncZero (X,Y)
now for x being Element of X holds ((FuncAdd (X,Y)) . (f,((FuncExtMult (X,Y)) . [(- jj),f]))) . x = (FuncZero (X,Y)) . xlet x be
Element of
X;
((FuncAdd (X,Y)) . (f,((FuncExtMult (X,Y)) . [(- jj),f]))) . x = (FuncZero (X,Y)) . xset y =
f . x;
thus ((FuncAdd (X,Y)) . (f,((FuncExtMult (X,Y)) . [(- jj),f]))) . x =
(f . x) + (((FuncExtMult (X,Y)) . [(- jj),f]) . x)
by Th1
.=
(f . x) + ((- 1) * (f . x))
by Th2
.=
(f . x) + (- (f . x))
by RLVECT_1:16
.=
0. Y
by RLVECT_1:5
.=
(FuncZero (X,Y)) . x
by FUNCOP_1:7
;
verum end;
hence
(FuncAdd (X,Y)) . (f,((FuncExtMult (X,Y)) . [(- 1),f])) = FuncZero (X,Y)
by FUNCT_2:63; verum