let X, Y, Z be RealLinearSpace; :: thesis: for f being LinearOperator of X,Y
for g being LinearOperator of Y,Z holds g * f is LinearOperator of X,Z
let f be LinearOperator of X,Y; :: thesis: for g being LinearOperator of Y,Z holds g * f is LinearOperator of X,Z
let g be LinearOperator of Y,Z; :: thesis: g * f is LinearOperator of X,Z

A1: now :: thesis: for v being VECTOR of X
for a being Real holds (g * f) . (a * v) = a * ((g * f) . v)

let v be VECTOR of X; :: thesis: for a being Real holds (g * f) . (a * v) = a * ((g * f) . v)
let a be Real; :: thesis: (g * f) . (a * v) = a * ((g * f) . v)
thus (g * f) . (a * v) = g . (f . (a * v)) by FUNCT_2:15
.= g . (a * (f . v)) by LOPBAN_1:def 5
.= a * (g . (f . v)) by LOPBAN_1:def 5
.= a * ((g * f) . v) by FUNCT_2:15 ; :: thesis: verum

end;

now :: thesis: for v, w being VECTOR of X holds (g * f) . (v + w) = ((g * f) . v) + ((g * f) . w)

let v, w be VECTOR of X; :: thesis: (g * f) . (v + w) = ((g * f) . v) + ((g * f) . w)
thus (g * f) . (v + w) = g . (f . (v + w)) by FUNCT_2:15
.= g . ((f . v) + (f . w)) by VECTSP_1:def 20
.= (g . (f . v)) + (g . (f . w)) by VECTSP_1:def 20
.= ((g * f) . v) + (g . (f . w)) by FUNCT_2:15
.= ((g * f) . v) + ((g * f) . w) by FUNCT_2:15 ; :: thesis: verum

end;

hence g * f is LinearOperator of X,Z by A1, LOPBAN_1:def 5, VECTSP_1:def 20; :: thesis: verum