set f = the carrier of X --> (0. Y);
A1: the carrier of X --> (0. Y) is homogeneous

proof

let x be VECTOR of X; :: according to CLOPBAN1:def 4 :: thesis: for r being Complex holds (the carrier of X --> (0. Y)) . (r * x) = r * ((the carrier of X --> (0. Y)) . x)
let c be Complex; :: thesis: (the carrier of X --> (0. Y)) . (c * x) = c * ((the carrier of X --> (0. Y)) . x)
thus (the carrier of X --> (0. Y)) . (c * x) = 0. Y by FUNCOP_1:13
.= c * (0. Y) by CLVECT_1:2
.= c * ((the carrier of X --> (0. Y)) . x) by FUNCOP_1:13 ; :: thesis: verum

end;

the carrier of X --> (0. Y) is additive

proof

let x, y be VECTOR of X; :: according to GRCAT_1:def 13 :: thesis: (the carrier of X --> (0. Y)) . (x + y) = ((the carrier of X --> (0. Y)) . x) + ((the carrier of X --> (0. Y)) . y)
thus (the carrier of X --> (0. Y)) . (x + y) = 0. Y by FUNCOP_1:13
.= (0. Y) + (0. Y) by RLVECT_1:10
.= ((the carrier of X --> (0. Y)) . x) + (0. Y) by FUNCOP_1:13
.= ((the carrier of X --> (0. Y)) . x) + ((the carrier of X --> (0. Y)) . y) by FUNCOP_1:13 ; :: thesis: verum

end;

hence not LinearOperators X,Y is empty by A1, Def5; :: thesis: LinearOperators X,Y is functional
let x be set ; :: according to FUNCT_1:def 19 :: thesis: ( not x in LinearOperators X,Y or x is set )
thus ( not x in LinearOperators X,Y or x is set ) ; :: thesis: verum