let X, Y, Z be RealLinearSpace; :: thesis: for L being LinearOperator of X,Y
for K being LinearOperator of Y,Z holds K * L is LinearOperator of X,Z
let L be LinearOperator of X,Y; :: thesis: for K being LinearOperator of Y,Z holds K * L is LinearOperator of X,Z
let K be LinearOperator of Y,Z; :: thesis: K * L is LinearOperator of X,Z
reconsider T = K * L as Function of X,Z ;
for x, y being Element of X holds T . (x + y) = (T . x) + (T . y)

proof

let x, y be Element of X; :: thesis: T . (x + y) = (T . x) + (T . y)
A1: L is additive ;
A2: K is additive ;
thus T . (x + y) = K . (L . (x + y)) by FUNCT_2:15
.= K . ((L . x) + (L . y)) by A1
.= (K . (L . x)) + (K . (L . y)) by A2
.= (T . x) + (K . (L . y)) by FUNCT_2:15
.= (T . x) + (T . y) by FUNCT_2:15 ; :: thesis: verum

end;

then A3: T is additive ;
for a being Real
for x being VECTOR of X holds T . (a * x) = a * (T . x)

proof

let a be Real; :: thesis: for x being VECTOR of X holds T . (a * x) = a * (T . x)
let x be VECTOR of X; :: thesis: T . (a * x) = a * (T . x)
thus T . (a * x) = K . (L . (a * x)) by FUNCT_2:15
.= K . (a * (L . x)) by LOPBAN_1:def 5
.= a * (K . (L . x)) by LOPBAN_1:def 5
.= a * (T . x) by FUNCT_2:15 ; :: thesis: verum

end;

then T is homogeneous ;
hence K * L is LinearOperator of X,Z by A3; :: thesis: verum