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

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