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 set ; :: 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 set such that
A1: ( z1 in the carrier of X & z1 in B0 + B1 & t = T . z1 ) by FUNCT_2:115;
consider x1, x2 being Element of X such that
A3: ( z1 = x1 + x2 & x1 in B0 & x2 in B1 ) by A1;
A4: t = (T . x1) + (T . x2) by A1, A3, LOPBAN_1:def 5;
A5: T . x1 in T .: B0 by A3, FUNCT_2:43;
T . x2 in T .: B1 by A3, FUNCT_2:43;
hence t in (T .: B0) + (T .: B1) by A4, A5; :: thesis: verum

end;

let t be set ; :: 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
P0: ( t = tz0 + tz1 & tz0 in T .: B0 & tz1 in T .: B1 ) ;
consider z0 being Element of the carrier of X such that
P1: ( z0 in B0 & tz0 = T . z0 ) by P0, FUNCT_2:116;
consider z1 being Element of the carrier of X such that
P2: ( z1 in B1 & tz1 = T . z1 ) by P0, FUNCT_2:116;
reconsider z0 = z0 as Point of X ;
reconsider z1 = z1 as Point of X ;
A2: z0 + z1 in B0 + B1 by P1, P2;
t = T . (z0 + z1) by P0, P1, P2, LOPBAN_1:def 5;
hence t in T .: (B0 + B1) by A2, FUNCT_2:43; :: thesis: verum