let V be RealLinearSpace; :: thesis: for u1, o, u, u2 being Element of V
for a3, c3, c2, a2, 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 u1, o, u, u2 be Element of V; :: thesis: for a3, c3, c2, a2, 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 a3, c3, c2, a2 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 9 ;
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 9 ;
(((((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 9 ;
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 9
.= (B1 * (((a3 * c2) - (a2 * c2)) " )) * (((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2)) by RLVECT_1:def 9 ;
:: thesis: verum