let V be RealLinearSpace; 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; 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; 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; ( 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)
; 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
;
verum