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

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)

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;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

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

hence
g * f is LinearOperator of X,Z
by A1, LOPBAN_1:def 5, VECTSP_1:def 20; :: thesis: verumlet 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;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