let V be RealLinearSpace; :: thesis: for o, u, u1, v1, u2, w2 being Element of V
for a2, c2, a3, c3, C2, C3 being Real st u1 = ((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2) & v1 = (o + (a3 * u)) + (c3 * u2) & w2 = (o + (a2 * u)) + (c2 * u2) & C2 + C3 = (a2 * c2) - (a3 * c3) & (C2 * a3) + (C3 * a2) = (a2 * a3) * (c2 - c3) & (C2 * c3) + (C3 * c2) = (c2 * c3) * (a2 - a3) holds
((1 * u1) + (C2 * v1)) + (C3 * w2) = 0. V
let o, u, u1, v1, u2, w2 be Element of V; :: thesis: for a2, c2, a3, c3, C2, C3 being Real st u1 = ((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2) & v1 = (o + (a3 * u)) + (c3 * u2) & w2 = (o + (a2 * u)) + (c2 * u2) & C2 + C3 = (a2 * c2) - (a3 * c3) & (C2 * a3) + (C3 * a2) = (a2 * a3) * (c2 - c3) & (C2 * c3) + (C3 * c2) = (c2 * c3) * (a2 - a3) holds
((1 * u1) + (C2 * v1)) + (C3 * w2) = 0. V
let a2, c2, a3, c3 be Real; :: thesis: for C2, C3 being Real st u1 = ((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2) & v1 = (o + (a3 * u)) + (c3 * u2) & w2 = (o + (a2 * u)) + (c2 * u2) & C2 + C3 = (a2 * c2) - (a3 * c3) & (C2 * a3) + (C3 * a2) = (a2 * a3) * (c2 - c3) & (C2 * c3) + (C3 * c2) = (c2 * c3) * (a2 - a3) holds
((1 * u1) + (C2 * v1)) + (C3 * w2) = 0. V
let C2, C3 be Real; :: thesis: ( u1 = ((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2) & v1 = (o + (a3 * u)) + (c3 * u2) & w2 = (o + (a2 * u)) + (c2 * u2) & C2 + C3 = (a2 * c2) - (a3 * c3) & (C2 * a3) + (C3 * a2) = (a2 * a3) * (c2 - c3) & (C2 * c3) + (C3 * c2) = (c2 * c3) * (a2 - a3) implies ((1 * u1) + (C2 * v1)) + (C3 * w2) = 0. V )
assume that
A1: u1 = ((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2) and
A2: ( v1 = (o + (a3 * u)) + (c3 * u2) & w2 = (o + (a2 * u)) + (c2 * u2) ) and
A3: ( C2 + C3 = (a2 * c2) - (a3 * c3) & (C2 * a3) + (C3 * a2) = (a2 * a3) * (c2 - c3) & (C2 * c3) + (C3 * c2) = (c2 * c3) * (a2 - a3) ) ; :: thesis: ((1 * u1) + (C2 * v1)) + (C3 * w2) = 0. V
A4: ((1 * u1) + (C2 * v1)) + (C3 * w2) = (u1 + (C2 * v1)) + (C3 * w2) by RLVECT_1:def 8
.= u1 + ((C2 * v1) + (C3 * w2)) by RLVECT_1:def 3 ;
(C2 * v1) + (C3 * w2) = ((C2 * (o + (a3 * u))) + (C2 * (c3 * u2))) + (C3 * ((o + (a2 * u)) + (c2 * u2))) by A2, RLVECT_1:def 5
.= (((C2 * o) + (C2 * (a3 * u))) + (C2 * (c3 * u2))) + (C3 * ((o + (a2 * u)) + (c2 * u2))) by RLVECT_1:def 5
.= (((C2 * o) + (C2 * (a3 * u))) + (C2 * (c3 * u2))) + ((C3 * (o + (a2 * u))) + (C3 * (c2 * u2))) by RLVECT_1:def 5
.= (((C2 * o) + (C2 * (a3 * u))) + (C2 * (c3 * u2))) + (((C3 * o) + (C3 * (a2 * u))) + (C3 * (c2 * u2))) by RLVECT_1:def 5
.= (((C2 * o) + (C3 * o)) + ((C2 * (a3 * u)) + (C3 * (a2 * u)))) + ((C2 * (c3 * u2)) + (C3 * (c2 * u2))) by Lm27
.= (((C2 + C3) * o) + ((C2 * (a3 * u)) + (C3 * (a2 * u)))) + ((C2 * (c3 * u2)) + (C3 * (c2 * u2))) by RLVECT_1:def 6
.= (((C2 + C3) * o) + (((C2 * a3) * u) + (C3 * (a2 * u)))) + ((C2 * (c3 * u2)) + (C3 * (c2 * u2))) by RLVECT_1:def 7
.= (((C2 + C3) * o) + (((C2 * a3) * u) + ((C3 * a2) * u))) + ((C2 * (c3 * u2)) + (C3 * (c2 * u2))) by RLVECT_1:def 7
.= (((C2 + C3) * o) + (((C2 * a3) * u) + ((C3 * a2) * u))) + (((C2 * c3) * u2) + (C3 * (c2 * u2))) by RLVECT_1:def 7
.= (((C2 + C3) * o) + (((C2 * a3) * u) + ((C3 * a2) * u))) + (((C2 * c3) * u2) + ((C3 * c2) * u2)) by RLVECT_1:def 7
.= (((C2 + C3) * o) + (((C2 * a3) + (C3 * a2)) * u)) + (((C2 * c3) * u2) + ((C3 * c2) * u2)) by RLVECT_1:def 6
.= ((((a2 * c2) - (a3 * c3)) * o) + (((a2 * a3) * (c2 - c3)) * u)) + (((c2 * c3) * (a2 - a3)) * u2) by A3, RLVECT_1:def 6 ;
hence ((1 * u1) + (C2 * v1)) + (C3 * w2) = (((((a3 * c3) - (a2 * c2)) * o) + (((a2 * c2) - (a3 * c3)) * o)) + ((((a2 * a3) * (c3 - c2)) * u) + (((a2 * a3) * (c2 - c3)) * u))) + ((((c2 * c3) * (a3 - a2)) * u2) + (((c2 * c3) * (a2 - a3)) * u2)) by A1, A4, Lm27
.= (((((a3 * c3) - (a2 * c2)) + ((a2 * c2) - (a3 * c3))) * o) + ((((a2 * a3) * (c3 - c2)) * u) + (((a2 * a3) * (c2 - c3)) * u))) + ((((c2 * c3) * (a3 - a2)) * u2) + (((c2 * c3) * (a2 - a3)) * u2)) by RLVECT_1:def 6
.= (((((a3 * c3) - (a2 * c2)) + ((a2 * c2) - (a3 * c3))) * o) + ((((a2 * a3) * (c3 - c2)) + ((a2 * a3) * (c2 - c3))) * u)) + ((((c2 * c3) * (a3 - a2)) * u2) + (((c2 * c3) * (a2 - a3)) * u2)) by RLVECT_1:def 6
.= ((((((a3 * c3) + (- (a2 * c2))) + (a2 * c2)) + (- (a3 * c3))) * o) + ((((a2 * a3) * (c3 - c2)) + ((a2 * a3) * (c2 - c3))) * u)) + ((((c2 * c3) * (a3 - a2)) + ((c2 * c3) * (a2 - a3))) * u2) by RLVECT_1:def 6
.= ((0. V) + ((((a2 * a3) * (c3 - c2)) + ((a2 * a3) * (c2 - c3))) * u)) + ((((c2 * c3) * (a3 - a2)) + ((c2 * c3) * (a2 - a3))) * u2) by RLVECT_1:10
.= (0 * u) + ((((c2 * c3) * (a3 - a2)) + (- ((c2 * c3) * (a3 - a2)))) * u2) by RLVECT_1:4
.= (0. V) + (0 * u2) by RLVECT_1:10
.= (0. V) + (0. V) by RLVECT_1:10
.= 0. V by RLVECT_1:4 ;
:: thesis: verum