let V be RealLinearSpace; :: thesis: for w2, o, u, u2, w1 being Element of V
for a2, c2, A3, A3', B3, B3' being Real st w2 = (o + (a2 * u)) + (c2 * u2) & w1 = ((B3 * o) + (A3 * u)) + ((B3 * c2) * u2) & B3 = B3' & A3 = B3' * a2 & B3 * c2 = A3' holds
w1 = B3 * w2
let w2, o, u, u2, w1 be Element of V; :: thesis: for a2, c2, A3, A3', B3, B3' being Real st w2 = (o + (a2 * u)) + (c2 * u2) & w1 = ((B3 * o) + (A3 * u)) + ((B3 * c2) * u2) & B3 = B3' & A3 = B3' * a2 & B3 * c2 = A3' holds
w1 = B3 * w2
let a2, c2 be Real; :: thesis: for A3, A3', B3, B3' being Real st w2 = (o + (a2 * u)) + (c2 * u2) & w1 = ((B3 * o) + (A3 * u)) + ((B3 * c2) * u2) & B3 = B3' & A3 = B3' * a2 & B3 * c2 = A3' holds
w1 = B3 * w2
let A3, A3', B3, B3' be Real; :: thesis: ( w2 = (o + (a2 * u)) + (c2 * u2) & w1 = ((B3 * o) + (A3 * u)) + ((B3 * c2) * u2) & B3 = B3' & A3 = B3' * a2 & B3 * c2 = A3' implies w1 = B3 * w2 )
assume A1: ( w2 = (o + (a2 * u)) + (c2 * u2) & w1 = ((B3 * o) + (A3 * u)) + ((B3 * c2) * u2) & B3 = B3' & A3 = B3' * a2 & B3 * c2 = A3' ) ; :: thesis: w1 = B3 * w2
hence w1 = ((B3 * o) + (B3 * (a2 * u))) + ((B3 * c2) * u2) by RLVECT_1:def 9
.= ((B3 * o) + (B3 * (a2 * u))) + (B3 * (c2 * u2)) by RLVECT_1:def 9
.= (B3 * (o + (a2 * u))) + (B3 * (c2 * u2)) by RLVECT_1:def 9
.= B3 * w2 by A1, RLVECT_1:def 9 ;
:: thesis: verum