theorem Th34: :: BKMODEL4:40

for l, r being Real
for u, v, w being Element of (TOP-REAL 3)
for n11, n12, n13, n21, n22, n23, n31, n32, n33, nu1, nu2, nu3, nv1, nv2, nv3, nw1, nw2, nw3 being Real st nu3 <> 0 & nv3 <> 0 & nw3 <> 0 & r = (l * nv3) / (((1 - l) * nu3) + (l * nv3)) & ((1 - l) * nu3) + (l * nv3) <> 0 & w = ((1 - l) * u) + (l * v) & nu1 = ((n11 * (u . 1)) + (n12 * (u . 2))) + n13 & nu2 = ((n21 * (u . 1)) + (n22 * (u . 2))) + n23 & nu3 = ((n31 * (u . 1)) + (n32 * (u . 2))) + n33 & nv1 = ((n11 * (v . 1)) + (n12 * (v . 2))) + n13 & nv2 = ((n21 * (v . 1)) + (n22 * (v . 2))) + n23 & nv3 = ((n31 * (v . 1)) + (n32 * (v . 2))) + n33 & nw1 = ((n11 * (w . 1)) + (n12 * (w . 2))) + n13 & nw2 = ((n21 * (w . 1)) + (n22 * (w . 2))) + n23 & nw3 = ((n31 * (w . 1)) + (n32 * (w . 2))) + n33 holds
((1 - r) * |[(nu1 / nu3),(nu2 / nu3),1]|) + (r * |[(nv1 / nv3),(nv2 / nv3),1]|) = |[(nw1 / nw3),(nw2 / nw3),1]|