let X be non empty set ; :: thesis: for Y being ComplexLinearSpace
for x being Element of X holds (FuncZero (X,Y)) . x = 0. Y
let Y be ComplexLinearSpace; :: thesis: for x being Element of X holds (FuncZero (X,Y)) . x = 0. Y
let x be Element of X; :: thesis: (FuncZero (X,Y)) . x = 0. Y
thus (FuncZero (X,Y)) . x = (X --> (0. Y)) . x by LOPBAN_1:def 3
.= 0. Y by FUNCOP_1:7 ; :: thesis: verum