let X, Y be RealLinearSpace; :: thesis: for f being LinearOperator of X,Y holds 0. Y = f . (0. X)
let f be LinearOperator of X,Y; :: thesis: 0. Y = f . (0. X)
(f /. (0. X)) + (0. Y) = f /. ((0. X) + (0. X))
.= (f /. (0. X)) + (f /. (0. X)) by VECTSP_1:def 20 ;
hence 0. Y = f . (0. X) by RLVECT_1:8; :: thesis: verum