let X, Y be ComplexLinearSpace; :: thesis: the carrier of X --> (0. Y) is LinearOperator of X,Y

set f = the carrier of X --> (0. Y);

reconsider f = the carrier of X --> (0. Y) as Function of X,Y ;

A1: f is homogeneous

set f = the carrier of X --> (0. Y);

reconsider f = the carrier of X --> (0. Y) as Function of X,Y ;

A1: f is homogeneous

proof

f is additive
let x be VECTOR of X; :: according to CLOPBAN1:def 3 :: thesis: for r being Complex holds f . (r * x) = r * (f . x)

let c be Complex; :: thesis: f . (c * x) = c * (f . x)

thus f . (c * x) = 0. Y by FUNCOP_1:7

.= c * (0. Y) by CLVECT_1:1

.= c * (f . x) by FUNCOP_1:7 ; :: thesis: verum

end;let c be Complex; :: thesis: f . (c * x) = c * (f . x)

thus f . (c * x) = 0. Y by FUNCOP_1:7

.= c * (0. Y) by CLVECT_1:1

.= c * (f . x) by FUNCOP_1:7 ; :: thesis: verum

proof

hence
the carrier of X --> (0. Y) is LinearOperator of X,Y
by A1; :: thesis: verum
let x, y be VECTOR of X; :: according to VECTSP_1:def 19 :: thesis: f . (x + y) = (f . x) + (f . y)

thus f . (x + y) = 0. Y by FUNCOP_1:7

.= (0. Y) + (0. Y) by RLVECT_1:4

.= (f . x) + (0. Y) by FUNCOP_1:7

.= (f . x) + (f . y) by FUNCOP_1:7 ; :: thesis: verum

end;thus f . (x + y) = 0. Y by FUNCOP_1:7

.= (0. Y) + (0. Y) by RLVECT_1:4

.= (f . x) + (0. Y) by FUNCOP_1:7

.= (f . x) + (f . y) by FUNCOP_1:7 ; :: thesis: verum