let X, Y be RealNormSpace; :: thesis: for T being LinearOperator of X,Y
for B0 being Subset of X
for x1 being Point of X holds T .: (x1 + B0) = (T . x1) + (T .: B0)
let T be LinearOperator of X,Y; :: thesis: for B0 being Subset of X
for x1 being Point of X holds T .: (x1 + B0) = (T . x1) + (T .: B0)
let B0 be Subset of X; :: thesis: for x1 being Point of X holds T .: (x1 + B0) = (T . x1) + (T .: B0)
let x1 be Point of X; :: thesis: T .: (x1 + B0) = (T . x1) + (T .: B0)
thus T .: (x1 + B0) c= (T . x1) + (T .: B0) :: according to XBOOLE_0:def 10 :: thesis: (T . x1) + (T .: B0) c= T .: (x1 + B0)

proof

let t be set ; :: according to TARSKI:def 3 :: thesis: ( not t in T .: (x1 + B0) or t in (T . x1) + (T .: B0) )
assume t in T .: (x1 + B0) ; :: thesis: t in (T . x1) + (T .: B0)
then consider z1 being set such that
A1: ( z1 in the carrier of X & z1 in x1 + B0 & t = T . z1 ) by FUNCT_2:115;
reconsider z1 = z1 as Point of X by A1;
consider z0 being Element of X such that
A3: ( z1 = x1 + z0 & z0 in B0 ) by A1;
A4: t = (T . x1) + (T . z0) by A1, A3, LOPBAN_1:def 5;
T . z0 in T .: B0 by A3, FUNCT_2:43;
hence t in (T . x1) + (T .: B0) by A4; :: thesis: verum

end;

let t be set ; :: according to TARSKI:def 3 :: thesis: ( not t in (T . x1) + (T .: B0) or t in T .: (x1 + B0) )
assume t in (T . x1) + (T .: B0) ; :: thesis: t in T .: (x1 + B0)
then consider tz0 being Point of Y such that
P0: ( t = (T . x1) + tz0 & tz0 in T .: B0 ) ;
consider z0 being Element of the carrier of X such that
P1: ( z0 in B0 & tz0 = T . z0 ) by P0, FUNCT_2:116;
A2: x1 + z0 in x1 + B0 by P1;
t = T . (x1 + z0) by P0, P1, LOPBAN_1:def 5;
hence t in T .: (x1 + B0) by A2, FUNCT_2:43; :: thesis: verum