let S, T be non trivial RealNormSpace; :: thesis: for R1 being REST of S st R1 /. 0 = 0. S holds
for R2 being REST of S,T st R2 /. (0. S) = 0. T holds
for L1 being LINEAR of S
for L2 being bounded LinearOperator of S,T holds (L2 * R1) + (R2 * (L1 + R1)) is REST of T
let R1 be REST of S; :: thesis: ( R1 /. 0 = 0. S implies for R2 being REST of S,T st R2 /. (0. S) = 0. T holds
for L1 being LINEAR of S
for L2 being bounded LinearOperator of S,T holds (L2 * R1) + (R2 * (L1 + R1)) is REST of T )
assume A1: R1 /. 0 = 0. S ; :: thesis: for R2 being REST of S,T st R2 /. (0. S) = 0. T holds
for L1 being LINEAR of S
for L2 being bounded LinearOperator of S,T holds (L2 * R1) + (R2 * (L1 + R1)) is REST of T
let R2 be REST of S,T; :: thesis: ( R2 /. (0. S) = 0. T implies for L1 being LINEAR of S
for L2 being bounded LinearOperator of S,T holds (L2 * R1) + (R2 * (L1 + R1)) is REST of T )
assume A2: R2 /. (0. S) = 0. T ; :: thesis: for L1 being LINEAR of S
for L2 being bounded LinearOperator of S,T holds (L2 * R1) + (R2 * (L1 + R1)) is REST of T
let L1 be LINEAR of S; :: thesis: for L2 being bounded LinearOperator of S,T holds (L2 * R1) + (R2 * (L1 + R1)) is REST of T
let L2 be bounded LinearOperator of S,T; :: thesis: (L2 * R1) + (R2 * (L1 + R1)) is REST of T
( L2 * R1 is REST of T & R2 * (L1 + R1) is REST of T ) by A1, A2, NDIFF211, NDIFF29;
hence (L2 * R1) + (R2 * (L1 + R1)) is REST of T by NDIFF_3:7; :: thesis: verum