let X, Y, Z be ComplexLinearSpace; :: 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

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:21
.= g . ((f . v) + (f . w)) by CLOPBAN1:def 3
.= (g . (f . v)) + (g . (f . w)) by CLOPBAN1:def 3
.= ((g * f) . v) + (g . (f . w)) by FUNCT_2:21
.= ((g * f) . v) + ((g * f) . w) by FUNCT_2:21 ; :: thesis: verum

end;

now

let v be VECTOR of X; :: thesis: for z being Complex holds (g * f) . (z * v) = z * ((g * f) . v)
let z be Complex; :: thesis: (g * f) . (z * v) = z * ((g * f) . v)
thus (g * f) . (z * v) = g . (f . (z * v)) by FUNCT_2:21
.= g . (z * (f . v)) by CLOPBAN1:def 4
.= z * (g . (f . v)) by CLOPBAN1:def 4
.= z * ((g * f) . v) by FUNCT_2:21 ; :: thesis: verum

end;

hence g * f is LinearOperator of X,Z by A1, CLOPBAN1:def 3, CLOPBAN1:def 4; :: thesis: verum