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

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