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

for B0 being Subset of X

for a being Real holds T .: (a * B0) = a * (T .: B0)

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

for a being Real holds T .: (a * B0) = a * (T .: B0)

let B0 be Subset of X; :: thesis: for a being Real holds T .: (a * B0) = a * (T .: B0)

let a be Real; :: thesis: T .: (a * B0) = a * (T .: B0)

thus T .: (a * B0) c= a * (T .: B0) :: according to XBOOLE_0:def 10 :: thesis: a * (T .: B0) c= T .: (a * B0)

assume t in a * (T .: B0) ; :: thesis: t in T .: (a * B0)

then consider tz0 being Point of Y such that

A6: t = a * tz0 and

A7: tz0 in T .: B0 ;

consider z0 being Element of X such that

A8: z0 in B0 and

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

reconsider z0 = z0 as Point of X ;

set z1 = a * z0;

A10: a * z0 in a * B0 by A8;

t = T . (a * z0) by A6, A9, LOPBAN_1:def 5;

hence t in T .: (a * B0) by A10, FUNCT_2:35; :: thesis: verum

for B0 being Subset of X

for a being Real holds T .: (a * B0) = a * (T .: B0)

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

for a being Real holds T .: (a * B0) = a * (T .: B0)

let B0 be Subset of X; :: thesis: for a being Real holds T .: (a * B0) = a * (T .: B0)

let a be Real; :: thesis: T .: (a * B0) = a * (T .: B0)

thus T .: (a * B0) c= a * (T .: B0) :: according to XBOOLE_0:def 10 :: thesis: a * (T .: B0) c= T .: (a * B0)

proof

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

assume t in T .: (a * B0) ; :: thesis: t in a * (T .: B0)

then consider z1 being object such that

z1 in the carrier of X and

A1: z1 in a * B0 and

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

consider x1 being Element of X such that

A3: z1 = a * x1 and

A4: x1 in B0 by A1;

A5: T . x1 in T .: B0 by A4, FUNCT_2:35;

t = a * (T . x1) by A2, A3, LOPBAN_1:def 5;

hence t in a * (T .: B0) by A5; :: thesis: verum

end;assume t in T .: (a * B0) ; :: thesis: t in a * (T .: B0)

then consider z1 being object such that

z1 in the carrier of X and

A1: z1 in a * B0 and

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

consider x1 being Element of X such that

A3: z1 = a * x1 and

A4: x1 in B0 by A1;

A5: T . x1 in T .: B0 by A4, FUNCT_2:35;

t = a * (T . x1) by A2, A3, LOPBAN_1:def 5;

hence t in a * (T .: B0) by A5; :: thesis: verum

assume t in a * (T .: B0) ; :: thesis: t in T .: (a * B0)

then consider tz0 being Point of Y such that

A6: t = a * tz0 and

A7: tz0 in T .: B0 ;

consider z0 being Element of X such that

A8: z0 in B0 and

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

reconsider z0 = z0 as Point of X ;

set z1 = a * z0;

A10: a * z0 in a * B0 by A8;

t = T . (a * z0) by A6, A9, LOPBAN_1:def 5;

hence t in T .: (a * B0) by A10, FUNCT_2:35; :: thesis: verum