let V be RealLinearSpace; for o, u, w1, u2, w2 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 o, u, w1, u2, w2 be 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 a2, c2 be Real; 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; ( 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 )
; 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
; verum