let V be RealLinearSpace; :: thesis: for o, u, u1, u2 being Element of V
for a2, c2, a3, c3, A1, B1 being Real st A1 = (((a3 * c3) - (a3 * c2)) * (((a3 * c2) - (a2 * c2)) ")) * B1 & c2 <> 0 & a2 <> a3 & u1 = (((A1 + B1) * o) + ((A1 * a2) * u)) + ((B1 * c3) * u2) holds
u1 = (B1 * (((a3 * c2) - (a2 * c2)) ")) * (((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2))
let o, u, u1, u2 be Element of V; :: thesis: for a2, c2, a3, c3, A1, B1 being Real st A1 = (((a3 * c3) - (a3 * c2)) * (((a3 * c2) - (a2 * c2)) ")) * B1 & c2 <> 0 & a2 <> a3 & u1 = (((A1 + B1) * o) + ((A1 * a2) * u)) + ((B1 * c3) * u2) holds
u1 = (B1 * (((a3 * c2) - (a2 * c2)) ")) * (((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2))
let a2, c2, a3, c3 be Real; :: thesis: for A1, B1 being Real st A1 = (((a3 * c3) - (a3 * c2)) * (((a3 * c2) - (a2 * c2)) ")) * B1 & c2 <> 0 & a2 <> a3 & u1 = (((A1 + B1) * o) + ((A1 * a2) * u)) + ((B1 * c3) * u2) holds
u1 = (B1 * (((a3 * c2) - (a2 * c2)) ")) * (((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2))
let A1, B1 be Real; :: thesis: ( A1 = (((a3 * c3) - (a3 * c2)) * (((a3 * c2) - (a2 * c2)) ")) * B1 & c2 <> 0 & a2 <> a3 & u1 = (((A1 + B1) * o) + ((A1 * a2) * u)) + ((B1 * c3) * u2) implies u1 = (B1 * (((a3 * c2) - (a2 * c2)) ")) * (((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2)) )
assume that
A1: A1 = (((a3 * c3) - (a3 * c2)) * (((a3 * c2) - (a2 * c2)) ")) * B1 and
A2: ( c2 <> 0 & a2 <> a3 ) and
A3: u1 = (((A1 + B1) * o) + ((A1 * a2) * u)) + ((B1 * c3) * u2) ; :: thesis: u1 = (B1 * (((a3 * c2) - (a2 * c2)) ")) * (((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2))
A4: (a3 * c2) - (a2 * c2) <> 0 by A2, Lm23;
A5: (B1 * c3) * u2 = ((B1 * 1) * c3) * u2
.= ((B1 * ((((a3 * c2) - (a2 * c2)) ") * ((a3 * c2) - (a2 * c2)))) * c3) * u2 by A4, XCMPLX_0:def 7
.= ((B1 * (((a3 * c2) - (a2 * c2)) ")) * ((c3 * c2) * (a3 - a2))) * u2
.= (B1 * (((a3 * c2) - (a2 * c2)) ")) * (((c2 * c3) * (a3 - a2)) * u2) by RLVECT_1:def 7 ;
A6: (((((a3 * c3) - (a3 * c2)) * (((a3 * c2) - (a2 * c2)) ")) * B1) * a2) * u = ((B1 * (((a3 * c2) - (a2 * c2)) ")) * ((a2 * a3) * (c3 - c2))) * u
.= (B1 * (((a3 * c2) - (a2 * c2)) ")) * (((a2 * a3) * (c3 - c2)) * u) by RLVECT_1:def 7 ;
(((((a3 * c3) - (a3 * c2)) * (((a3 * c2) - (a2 * c2)) ")) * B1) + (B1 * 1)) * o = ((((a3 * c3) - (a3 * c2)) * (B1 * (((a3 * c2) - (a2 * c2)) "))) + (B1 * ((((a3 * c2) - (a2 * c2)) ") * ((a3 * c2) - (a2 * c2))))) * o by A4, XCMPLX_0:def 7
.= ((B1 * (((a3 * c2) - (a2 * c2)) ")) * ((((a3 * c3) + (- (a3 * c2))) + (a3 * c2)) - (a2 * c2))) * o
.= (B1 * (((a3 * c2) - (a2 * c2)) ")) * (((a3 * c3) - (a2 * c2)) * o) by RLVECT_1:def 7 ;
hence u1 = ((B1 * (((a3 * c2) - (a2 * c2)) ")) * ((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u))) + ((B1 * (((a3 * c2) - (a2 * c2)) ")) * (((c2 * c3) * (a3 - a2)) * u2)) by A1, A3, A6, A5, RLVECT_1:def 5
.= (B1 * (((a3 * c2) - (a2 * c2)) ")) * (((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2)) by RLVECT_1:def 5 ;
:: thesis: verum