let a be non zero Real; :: thesis: for b, c being Real holds a * |[(b / a),(c / a),1]| = |[b,c,a]|
let b, c be Real; :: thesis: a * |[(b / a),(c / a),1]| = |[b,c,a]|
a * |[(b / a),(c / a),1]| = |[(a * (b / a)),(a * (c / a)),(a * 1)]| by EUCLID_5:8
.= |[b,(a * (c / a)),a]| by XCMPLX_1:87
.= |[b,c,a]| by XCMPLX_1:87 ;
hence a * |[(b / a),(c / a),1]| = |[b,c,a]| ; :: thesis: verum