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 :: thesis: for v being VECTOR of X
for z being Complex holds (g * f) . (z * v) = z * ((g * f) . v)
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:15
.= g . (z * (f . v)) by CLOPBAN1:def 3
.= z * (g . (f . v)) by CLOPBAN1:def 3
.= z * ((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, CLOPBAN1:def 3, VECTSP_1:def 20; :: thesis: verum