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

A1: the carrier of X --> (0. Y) is homogeneous

let x be object ; :: according to FUNCT_1:def 13 :: thesis: ( not x in LinearOperators (X,Y) or x is set )

thus ( not x in LinearOperators (X,Y) or x is set ) ; :: thesis: verum

A1: the carrier of X --> (0. Y) is homogeneous

proof

the carrier of X --> (0. Y) is additive
let x be VECTOR of X; :: according to CLOPBAN1:def 3 :: 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:7

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

.= c * (( the carrier of X --> (0. Y)) . x) by FUNCOP_1:7 ; :: thesis: verum

end;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:7

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

.= c * (( the carrier of X --> (0. Y)) . x) by FUNCOP_1:7 ; :: thesis: verum

proof

hence
not LinearOperators (X,Y) is empty
by A1, Def4; :: thesis: LinearOperators (X,Y) is functional
let x, y be VECTOR of X; :: according to VECTSP_1:def 19 :: 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:7

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

.= (( the carrier of X --> (0. Y)) . x) + (0. Y) by FUNCOP_1:7

.= (( the carrier of X --> (0. Y)) . x) + (( the carrier of X --> (0. Y)) . y) by FUNCOP_1:7 ; :: thesis: verum

end;thus ( the carrier of X --> (0. Y)) . (x + y) = 0. Y by FUNCOP_1:7

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

.= (( the carrier of X --> (0. Y)) . x) + (0. Y) by FUNCOP_1:7

.= (( the carrier of X --> (0. Y)) . x) + (( the carrier of X --> (0. Y)) . y) by FUNCOP_1:7 ; :: thesis: verum

let x be object ; :: according to FUNCT_1:def 13 :: thesis: ( not x in LinearOperators (X,Y) or x is set )

thus ( not x in LinearOperators (X,Y) or x is set ) ; :: thesis: verum