let X, Y be RealNormSpace; :: 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) by RLVECT_1:4
.= f /. ((0. X) + (0. X)) by RLVECT_1:4
.= (f /. (0. X)) + (f /. (0. X)) by VECTSP_1:def 20 ;
hence 0. Y = f . (0. X) by RLVECT_1:8; :: thesis: verum