let X, Y be RealNormSpace; :: thesis: for T being LinearOperator of X,Y

for B0, B1 being Subset of X holds T .: (B0 + B1) = (T .: B0) + (T .: B1)

let T be LinearOperator of X,Y; :: thesis: for B0, B1 being Subset of X holds T .: (B0 + B1) = (T .: B0) + (T .: B1)

let B0, B1 be Subset of X; :: thesis: T .: (B0 + B1) = (T .: B0) + (T .: B1)

thus T .: (B0 + B1) c= (T .: B0) + (T .: B1) :: according to XBOOLE_0:def 10 :: thesis: (T .: B0) + (T .: B1) c= T .: (B0 + B1)

assume t in (T .: B0) + (T .: B1) ; :: thesis: t in T .: (B0 + B1)

then consider tz0, tz1 being Point of Y such that

A6: t = tz0 + tz1 and

A7: tz0 in T .: B0 and

A8: tz1 in T .: B1 ;

consider z1 being Element of X such that

A9: z1 in B1 and

A10: tz1 = T . z1 by A8, FUNCT_2:65;

consider z0 being Element of X such that

A11: z0 in B0 and

A12: tz0 = T . z0 by A7, FUNCT_2:65;

reconsider z1 = z1 as Point of X ;

reconsider z0 = z0 as Point of X ;

A13: z0 + z1 in B0 + B1 by A11, A9;

t = T . (z0 + z1) by A6, A12, A10, VECTSP_1:def 20;

hence t in T .: (B0 + B1) by A13, FUNCT_2:35; :: thesis: verum

for B0, B1 being Subset of X holds T .: (B0 + B1) = (T .: B0) + (T .: B1)

let T be LinearOperator of X,Y; :: thesis: for B0, B1 being Subset of X holds T .: (B0 + B1) = (T .: B0) + (T .: B1)

let B0, B1 be Subset of X; :: thesis: T .: (B0 + B1) = (T .: B0) + (T .: B1)

thus T .: (B0 + B1) c= (T .: B0) + (T .: B1) :: according to XBOOLE_0:def 10 :: thesis: (T .: B0) + (T .: B1) c= T .: (B0 + B1)

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in (T .: B0) + (T .: B1) or t in T .: (B0 + B1) )
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in T .: (B0 + B1) or t in (T .: B0) + (T .: B1) )

assume t in T .: (B0 + B1) ; :: thesis: t in (T .: B0) + (T .: B1)

then consider z1 being object such that

z1 in the carrier of X and

A1: z1 in B0 + B1 and

A2: t = T . z1 by FUNCT_2:64;

consider x1, x2 being Element of X such that

A3: z1 = x1 + x2 and

A4: ( x1 in B0 & x2 in B1 ) by A1;

A5: ( T . x1 in T .: B0 & T . x2 in T .: B1 ) by A4, FUNCT_2:35;

t = (T . x1) + (T . x2) by A2, A3, VECTSP_1:def 20;

hence t in (T .: B0) + (T .: B1) by A5; :: thesis: verum

end;assume t in T .: (B0 + B1) ; :: thesis: t in (T .: B0) + (T .: B1)

then consider z1 being object such that

z1 in the carrier of X and

A1: z1 in B0 + B1 and

A2: t = T . z1 by FUNCT_2:64;

consider x1, x2 being Element of X such that

A3: z1 = x1 + x2 and

A4: ( x1 in B0 & x2 in B1 ) by A1;

A5: ( T . x1 in T .: B0 & T . x2 in T .: B1 ) by A4, FUNCT_2:35;

t = (T . x1) + (T . x2) by A2, A3, VECTSP_1:def 20;

hence t in (T .: B0) + (T .: B1) by A5; :: thesis: verum

assume t in (T .: B0) + (T .: B1) ; :: thesis: t in T .: (B0 + B1)

then consider tz0, tz1 being Point of Y such that

A6: t = tz0 + tz1 and

A7: tz0 in T .: B0 and

A8: tz1 in T .: B1 ;

consider z1 being Element of X such that

A9: z1 in B1 and

A10: tz1 = T . z1 by A8, FUNCT_2:65;

consider z0 being Element of X such that

A11: z0 in B0 and

A12: tz0 = T . z0 by A7, FUNCT_2:65;

reconsider z1 = z1 as Point of X ;

reconsider z0 = z0 as Point of X ;

A13: z0 + z1 in B0 + B1 by A11, A9;

t = T . (z0 + z1) by A6, A12, A10, VECTSP_1:def 20;

hence t in T .: (B0 + B1) by A13, FUNCT_2:35; :: thesis: verum