let X, Y be RealNormSpace; :: thesis: for a being Real
for v1, v2 being Lipschitzian LinearOperator of X,Y
for w1, w2 being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st v1 = w1 & v2 = w2 holds
( v1 + v2 = w1 + w2 & a (#) v1 = a * w1 )
let a be Real; :: thesis: for v1, v2 being Lipschitzian LinearOperator of X,Y
for w1, w2 being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st v1 = w1 & v2 = w2 holds
( v1 + v2 = w1 + w2 & a (#) v1 = a * w1 )
let v1, v2 be Lipschitzian LinearOperator of X,Y; :: thesis: for w1, w2 being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st v1 = w1 & v2 = w2 holds
( v1 + v2 = w1 + w2 & a (#) v1 = a * w1 )
let zw1, zw2 be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: ( v1 = zw1 & v2 = zw2 implies ( v1 + v2 = zw1 + zw2 & a (#) v1 = a * zw1 ) )
assume A1: ( v1 = zw1 & v2 = zw2 ) ; :: thesis: ( v1 + v2 = zw1 + zw2 & a (#) v1 = a * zw1 )
reconsider zw12 = zw1 + zw2 as Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) ;
zw12 is Lipschitzian LinearOperator of X,Y by LOPBAN_1:def 9;
then A2: dom zw12 = the carrier of X by FUNCT_2:def 1;
A3: dom (v1 + v2) = (dom v1) /\ (dom v2) by VFUNCT_1:def 1
.= the carrier of X /\ (dom v2) by FUNCT_2:def 1
.= the carrier of X /\ the carrier of X by FUNCT_2:def 1
.= the carrier of X ;
for s being object st s in dom (v1 + v2) holds
(v1 + v2) . s = zw12 . s

proof

let s be object ; :: thesis: ( s in dom (v1 + v2) implies (v1 + v2) . s = zw12 . s )
assume A4: s in dom (v1 + v2) ; :: thesis: (v1 + v2) . s = zw12 . s
then reconsider d = s as Point of X ;
thus (v1 + v2) . s = (v1 + v2) /. d by A3, PARTFUN1:def 6
.= (v1 /. d) + (v2 /. d) by A4, VFUNCT_1:def 1
.= zw12 . s by A1, LOPBAN_1:35 ; :: thesis: verum

end;

hence v1 + v2 = zw1 + zw2 by A2, A3, FUNCT_1:2; :: thesis: a (#) v1 = a * zw1
reconsider zw12 = a * zw1 as Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) ;
zw12 is Lipschitzian LinearOperator of X,Y by LOPBAN_1:def 9;
then A5: dom zw12 = the carrier of X by FUNCT_2:def 1;
A6: dom (a (#) v1) = dom v1 by VFUNCT_1:def 4
.= the carrier of X by FUNCT_2:def 1 ;
for s being object st s in dom (a (#) v1) holds
(a (#) v1) . s = zw12 . s

proof

let s be object ; :: thesis: ( s in dom (a (#) v1) implies (a (#) v1) . s = zw12 . s )
assume A7: s in dom (a (#) v1) ; :: thesis: (a (#) v1) . s = zw12 . s
then reconsider d = s as Point of X ;
thus (a (#) v1) . s = (a (#) v1) /. d by A6, PARTFUN1:def 6
.= a * (v1 /. d) by A7, VFUNCT_1:def 4
.= zw12 . s by A1, LOPBAN_1:36 ; :: thesis: verum

end;

hence a (#) v1 = a * zw1 by A5, A6, FUNCT_1:2; :: thesis: verum