let a, b, c, d, e, f, r be Real; :: thesis: ( ((1 - r) * |[a,b,1]|) + (r * |[c,d,1]|) = |[e,f,1]| implies ((1 - r) * |[a,b]|) + (r * |[c,d]|) = |[e,f]| )
assume ((1 - r) * |[a,b,1]|) + (r * |[c,d,1]|) = |[e,f,1]| ; :: thesis: ((1 - r) * |[a,b]|) + (r * |[c,d]|) = |[e,f]|
then |[e,f,1]| = |[((1 - r) * a),((1 - r) * b),((1 - r) * 1)]| + (r * |[c,d,1]|) by EUCLID_5:8
.= |[((1 - r) * a),((1 - r) * b),(1 - r)]| + |[(r * c),(r * d),(r * 1)]| by EUCLID_5:8
.= |[(((1 - r) * a) + (r * c)),(((1 - r) * b) + (r * d)),((1 - r) + r)]| by EUCLID_5:6 ;
then ( e = ((1 - r) * a) + (r * c) & f = ((1 - r) * b) + (r * d) ) by FINSEQ_1:78;
then |[e,f]| = |[((1 - r) * a),((1 - r) * b)]| + |[(r * c),(r * d)]| by EUCLID:56
.= ((1 - r) * |[a,b]|) + |[(r * c),(r * d)]| by EUCLID:58
.= ((1 - r) * |[a,b]|) + (r * |[c,d]|) by EUCLID:58 ;
hence ((1 - r) * |[a,b]|) + (r * |[c,d]|) = |[e,f]| ; :: thesis: verum