let V be RealLinearSpace; :: thesis: for w2, o, u, u2, w1 being Element of V
for a2, c2, A3, A39, B3, B39 being Real st w2 = (o + (a2 * u)) + (c2 * u2) & w1 = ((B3 * o) + (A3 * u)) + ((B3 * c2) * u2) & B3 = B39 & A3 = B39 * a2 holds
w1 = B3 * w2
let w2, o, u, u2, w1 be Element of V; :: thesis: for a2, c2, A3, A39, B3, B39 being Real st w2 = (o + (a2 * u)) + (c2 * u2) & w1 = ((B3 * o) + (A3 * u)) + ((B3 * c2) * u2) & B3 = B39 & A3 = B39 * a2 holds
w1 = B3 * w2
let a2, c2 be Real; :: thesis: for A3, A39, B3, B39 being Real st w2 = (o + (a2 * u)) + (c2 * u2) & w1 = ((B3 * o) + (A3 * u)) + ((B3 * c2) * u2) & B3 = B39 & A3 = B39 * a2 holds
w1 = B3 * w2
let A3, A39, B3, B39 be Real; :: thesis: ( w2 = (o + (a2 * u)) + (c2 * u2) & w1 = ((B3 * o) + (A3 * u)) + ((B3 * c2) * u2) & B3 = B39 & A3 = B39 * a2 implies w1 = B3 * w2 )
assume that
A1: w2 = (o + (a2 * u)) + (c2 * u2) and
A2: ( w1 = ((B3 * o) + (A3 * u)) + ((B3 * c2) * u2) & B3 = B39 & A3 = B39 * a2 ) ; :: thesis: w1 = B3 * w2
thus w1 = ((B3 * o) + (B3 * (a2 * u))) + ((B3 * c2) * u2) by A2, RLVECT_1:def 7
.= ((B3 * o) + (B3 * (a2 * u))) + (B3 * (c2 * u2)) by RLVECT_1:def 7
.= (B3 * (o + (a2 * u))) + (B3 * (c2 * u2)) by RLVECT_1:def 5
.= B3 * w2 by A1, RLVECT_1:def 5 ; :: thesis: verum