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)
proof
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;
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in (T .: B0) + (T .: B1) or t in 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