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

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