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
let x be VECTOR of X; :: according to LOPBAN_1:def 5 :: thesis: for r being Real holds f . (r * x) = r * (f . x)
let r be Real; :: thesis: f . (r * x) = r * (f . x)
thus f . (r * x) = 0. Y by FUNCOP_1:7
.= r * (0. Y)
.= r * (f . x) by FUNCOP_1:7 ; :: thesis: verum
end;
f is additive
proof
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)
.= (f . x) + (0. Y) by FUNCOP_1:7
.= (f . x) + (f . y) by FUNCOP_1:7 ; :: thesis: verum
end;
hence not LinearOperators (X,Y) is empty by A1, Def6; :: thesis: LinearOperators (X,Y) is functional
let x be object ; :: according to FUNCT_1:def 13 :: thesis: ( not x in LinearOperators (X,Y) or x is set )
assume x in LinearOperators (X,Y) ; :: thesis: x is set
hence x is set ; :: thesis: verum