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)

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

then consider tz0 being Point of Y such that

A7: t = (T . x1) + tz0 and

A8: tz0 in T .: B0 ;

consider z0 being Element of X such that

A9: z0 in B0 and

A10: tz0 = T . z0 by A8, FUNCT_2:65;

A11: x1 + z0 in x1 + B0 by A9;

t = T . (x1 + z0) by A7, A10, VECTSP_1:def 20;

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

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

A1: z1 in the carrier of X and

A2: z1 in x1 + B0 and

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

reconsider z1 = z1 as Point of X by A1;

consider z0 being Element of X such that

A4: z1 = x1 + z0 and

A5: z0 in B0 by A2;

A6: T . z0 in T .: B0 by A5, FUNCT_2:35;

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

hence t in (T . x1) + (T .: B0) by A6; :: thesis: verum

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

then consider z1 being object such that

A1: z1 in the carrier of X and

A2: z1 in x1 + B0 and

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

reconsider z1 = z1 as Point of X by A1;

consider z0 being Element of X such that

A4: z1 = x1 + z0 and

A5: z0 in B0 by A2;

A6: T . z0 in T .: B0 by A5, FUNCT_2:35;

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

hence t in (T . x1) + (T .: B0) by A6; :: thesis: verum

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

then consider tz0 being Point of Y such that

A7: t = (T . x1) + tz0 and

A8: tz0 in T .: B0 ;

consider z0 being Element of X such that

A9: z0 in B0 and

A10: tz0 = T . z0 by A8, FUNCT_2:65;

A11: x1 + z0 in x1 + B0 by A9;

t = T . (x1 + z0) by A7, A10, VECTSP_1:def 20;

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