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) . (FuncZero X,Y),f = f
let Y be ComplexLinearSpace; :: thesis: for f being Element of Funcs X,the carrier of Y holds (FuncAdd X,Y) . (FuncZero X,Y),f = f
let f be Element of Funcs X,the carrier of Y; :: thesis: (FuncAdd X,Y) . (FuncZero X,Y),f = f

now

let x be Element of X; :: thesis: ((FuncAdd X,Y) . (FuncZero X,Y),f) . x = f . x
thus ((FuncAdd X,Y) . (FuncZero X,Y),f) . x = ((FuncZero X,Y) . x) + (f . x) by LOPBAN_1:3
.= (0. Y) + (f . x) by Th2
.= f . x by RLVECT_1:def 7 ; :: thesis: verum

end;

hence (FuncAdd X,Y) . (FuncZero X,Y),f = f by FUNCT_2:113; :: thesis: verum