let V be RealLinearSpace; :: thesis: for u, w, y being Element of V
for a, b, c, d, e, f, A, B, C being Real holds ((A * ((a * u) + (b * w))) + (B * ((c * w) + (d * y)))) + (C * ((e * u) + (f * y))) = ((((A * a) + (C * e)) * u) + (((A * b) + (B * c)) * w)) + (((B * d) + (C * f)) * y)
let u, w, y be Element of V; :: thesis: for a, b, c, d, e, f, A, B, C being Real holds ((A * ((a * u) + (b * w))) + (B * ((c * w) + (d * y)))) + (C * ((e * u) + (f * y))) = ((((A * a) + (C * e)) * u) + (((A * b) + (B * c)) * w)) + (((B * d) + (C * f)) * y)
let a, b, c, d, e, f be Real; :: thesis: for A, B, C being Real holds ((A * ((a * u) + (b * w))) + (B * ((c * w) + (d * y)))) + (C * ((e * u) + (f * y))) = ((((A * a) + (C * e)) * u) + (((A * b) + (B * c)) * w)) + (((B * d) + (C * f)) * y)
let A, B, C be Real; :: thesis: ((A * ((a * u) + (b * w))) + (B * ((c * w) + (d * y)))) + (C * ((e * u) + (f * y))) = ((((A * a) + (C * e)) * u) + (((A * b) + (B * c)) * w)) + (((B * d) + (C * f)) * y)
A1: C * ((e * u) + (f * y)) = ((C * e) * u) + ((C * f) * y) by Lm7;
( A * ((a * u) + (b * w)) = ((A * a) * u) + ((A * b) * w) & B * ((c * w) + (d * y)) = ((B * c) * w) + ((B * d) * y) ) by Lm7;
hence ((A * ((a * u) + (b * w))) + (B * ((c * w) + (d * y)))) + (C * ((e * u) + (f * y))) = (((((A * a) * u) + ((A * b) * w)) + ((B * c) * w)) + ((B * d) * y)) + (((C * e) * u) + ((C * f) * y)) by A1, RLVECT_1:def 3
.= ((((A * a) * u) + (((A * b) * w) + ((B * c) * w))) + ((B * d) * y)) + (((C * e) * u) + ((C * f) * y)) by RLVECT_1:def 3
.= ((((A * a) * u) + (((A * b) + (B * c)) * w)) + ((B * d) * y)) + (((C * e) * u) + ((C * f) * y)) by RLVECT_1:def 6
.= (((A * a) * u) + (((A * b) + (B * c)) * w)) + (((B * d) * y) + (((C * f) * y) + ((C * e) * u))) by RLVECT_1:def 3
.= (((A * a) * u) + (((A * b) + (B * c)) * w)) + ((((B * d) * y) + ((C * f) * y)) + ((C * e) * u)) by RLVECT_1:def 3
.= (((A * a) * u) + (((A * b) + (B * c)) * w)) + ((((B * d) + (C * f)) * y) + ((C * e) * u)) by RLVECT_1:def 6
.= ((A * a) * u) + ((((A * b) + (B * c)) * w) + ((((B * d) + (C * f)) * y) + ((C * e) * u))) by RLVECT_1:def 3
.= ((A * a) * u) + (((C * e) * u) + ((((A * b) + (B * c)) * w) + (((B * d) + (C * f)) * y))) by RLVECT_1:def 3
.= (((A * a) * u) + ((C * e) * u)) + ((((A * b) + (B * c)) * w) + (((B * d) + (C * f)) * y)) by RLVECT_1:def 3
.= (((A * a) + (C * e)) * u) + ((((A * b) + (B * c)) * w) + (((B * d) + (C * f)) * y)) by RLVECT_1:def 6
.= ((((A * a) + (C * e)) * u) + (((A * b) + (B * c)) * w)) + (((B * d) + (C * f)) * y) by RLVECT_1:def 3 ;
:: thesis: verum