let K be Field; :: thesis: for a1, a2, a3, a4 being Element of K holds
( a1 * ((a2 + a3) + a4) = ((a1 * a2) + (a1 * a3)) + (a1 * a4) & a1 * ((a2 + a3) - a4) = ((a1 * a2) + (a1 * a3)) - (a1 * a4) & a1 * ((a2 - a3) + a4) = ((a1 * a2) - (a1 * a3)) + (a1 * a4) & a1 * ((a2 - a3) - a4) = ((a1 * a2) - (a1 * a3)) - (a1 * a4) & a1 * (((- a2) + a3) + a4) = ((- (a1 * a2)) + (a1 * a3)) + (a1 * a4) & a1 * (((- a2) + a3) - a4) = ((- (a1 * a2)) + (a1 * a3)) - (a1 * a4) & a1 * (((- a2) - a3) + a4) = ((- (a1 * a2)) - (a1 * a3)) + (a1 * a4) & a1 * (((- a2) - a3) - a4) = ((- (a1 * a2)) - (a1 * a3)) - (a1 * a4) )
let a1, a2, a3, a4 be Element of K; :: thesis: ( a1 * ((a2 + a3) + a4) = ((a1 * a2) + (a1 * a3)) + (a1 * a4) & a1 * ((a2 + a3) - a4) = ((a1 * a2) + (a1 * a3)) - (a1 * a4) & a1 * ((a2 - a3) + a4) = ((a1 * a2) - (a1 * a3)) + (a1 * a4) & a1 * ((a2 - a3) - a4) = ((a1 * a2) - (a1 * a3)) - (a1 * a4) & a1 * (((- a2) + a3) + a4) = ((- (a1 * a2)) + (a1 * a3)) + (a1 * a4) & a1 * (((- a2) + a3) - a4) = ((- (a1 * a2)) + (a1 * a3)) - (a1 * a4) & a1 * (((- a2) - a3) + a4) = ((- (a1 * a2)) - (a1 * a3)) + (a1 * a4) & a1 * (((- a2) - a3) - a4) = ((- (a1 * a2)) - (a1 * a3)) - (a1 * a4) )
thus a1 * ((a2 + a3) + a4) = (a1 * (a2 + a3)) + (a1 * a4) by VECTSP_1:4
.= ((a1 * a2) + (a1 * a3)) + (a1 * a4) by VECTSP_1:4 ; :: thesis: ( a1 * ((a2 + a3) - a4) = ((a1 * a2) + (a1 * a3)) - (a1 * a4) & a1 * ((a2 - a3) + a4) = ((a1 * a2) - (a1 * a3)) + (a1 * a4) & a1 * ((a2 - a3) - a4) = ((a1 * a2) - (a1 * a3)) - (a1 * a4) & a1 * (((- a2) + a3) + a4) = ((- (a1 * a2)) + (a1 * a3)) + (a1 * a4) & a1 * (((- a2) + a3) - a4) = ((- (a1 * a2)) + (a1 * a3)) - (a1 * a4) & a1 * (((- a2) - a3) + a4) = ((- (a1 * a2)) - (a1 * a3)) + (a1 * a4) & a1 * (((- a2) - a3) - a4) = ((- (a1 * a2)) - (a1 * a3)) - (a1 * a4) )
thus a1 * ((a2 + a3) - a4) = (a1 * (a2 + a3)) + (a1 * (- a4)) by VECTSP_1:4
.= ((a1 * a2) + (a1 * a3)) + (a1 * (- a4)) by VECTSP_1:4
.= ((a1 * a2) + (a1 * a3)) - (a1 * a4) by VECTSP_1:8 ; :: thesis: ( a1 * ((a2 - a3) + a4) = ((a1 * a2) - (a1 * a3)) + (a1 * a4) & a1 * ((a2 - a3) - a4) = ((a1 * a2) - (a1 * a3)) - (a1 * a4) & a1 * (((- a2) + a3) + a4) = ((- (a1 * a2)) + (a1 * a3)) + (a1 * a4) & a1 * (((- a2) + a3) - a4) = ((- (a1 * a2)) + (a1 * a3)) - (a1 * a4) & a1 * (((- a2) - a3) + a4) = ((- (a1 * a2)) - (a1 * a3)) + (a1 * a4) & a1 * (((- a2) - a3) - a4) = ((- (a1 * a2)) - (a1 * a3)) - (a1 * a4) )
thus a1 * ((a2 - a3) + a4) = (a1 * (a2 + (- a3))) + (a1 * a4) by VECTSP_1:4
.= ((a1 * a2) + (a1 * (- a3))) + (a1 * a4) by VECTSP_1:4
.= ((a1 * a2) - (a1 * a3)) + (a1 * a4) by VECTSP_1:8 ; :: thesis: ( a1 * ((a2 - a3) - a4) = ((a1 * a2) - (a1 * a3)) - (a1 * a4) & a1 * (((- a2) + a3) + a4) = ((- (a1 * a2)) + (a1 * a3)) + (a1 * a4) & a1 * (((- a2) + a3) - a4) = ((- (a1 * a2)) + (a1 * a3)) - (a1 * a4) & a1 * (((- a2) - a3) + a4) = ((- (a1 * a2)) - (a1 * a3)) + (a1 * a4) & a1 * (((- a2) - a3) - a4) = ((- (a1 * a2)) - (a1 * a3)) - (a1 * a4) )
thus a1 * ((a2 - a3) - a4) = (a1 * (a2 + (- a3))) + (a1 * (- a4)) by VECTSP_1:4
.= ((a1 * a2) + (a1 * (- a3))) + (a1 * (- a4)) by VECTSP_1:4
.= ((a1 * a2) - (a1 * a3)) + (a1 * (- a4)) by VECTSP_1:8
.= ((a1 * a2) - (a1 * a3)) - (a1 * a4) by VECTSP_1:8 ; :: thesis: ( a1 * (((- a2) + a3) + a4) = ((- (a1 * a2)) + (a1 * a3)) + (a1 * a4) & a1 * (((- a2) + a3) - a4) = ((- (a1 * a2)) + (a1 * a3)) - (a1 * a4) & a1 * (((- a2) - a3) + a4) = ((- (a1 * a2)) - (a1 * a3)) + (a1 * a4) & a1 * (((- a2) - a3) - a4) = ((- (a1 * a2)) - (a1 * a3)) - (a1 * a4) )
thus a1 * (((- a2) + a3) + a4) = (a1 * ((- a2) + a3)) + (a1 * a4) by VECTSP_1:4
.= ((a1 * (- a2)) + (a1 * a3)) + (a1 * a4) by VECTSP_1:4
.= ((- (a1 * a2)) + (a1 * a3)) + (a1 * a4) by VECTSP_1:8 ; :: thesis: ( a1 * (((- a2) + a3) - a4) = ((- (a1 * a2)) + (a1 * a3)) - (a1 * a4) & a1 * (((- a2) - a3) + a4) = ((- (a1 * a2)) - (a1 * a3)) + (a1 * a4) & a1 * (((- a2) - a3) - a4) = ((- (a1 * a2)) - (a1 * a3)) - (a1 * a4) )
thus a1 * (((- a2) + a3) - a4) = (a1 * ((- a2) + a3)) + (a1 * (- a4)) by VECTSP_1:4
.= ((a1 * (- a2)) + (a1 * a3)) + (a1 * (- a4)) by VECTSP_1:4
.= ((- (a1 * a2)) + (a1 * a3)) + (a1 * (- a4)) by VECTSP_1:8
.= ((- (a1 * a2)) + (a1 * a3)) - (a1 * a4) by VECTSP_1:8 ; :: thesis: ( a1 * (((- a2) - a3) + a4) = ((- (a1 * a2)) - (a1 * a3)) + (a1 * a4) & a1 * (((- a2) - a3) - a4) = ((- (a1 * a2)) - (a1 * a3)) - (a1 * a4) )
thus a1 * (((- a2) - a3) + a4) = (a1 * ((- a2) + (- a3))) + (a1 * a4) by VECTSP_1:4
.= ((a1 * (- a2)) + (a1 * (- a3))) + (a1 * a4) by VECTSP_1:4
.= ((- (a1 * a2)) + (a1 * (- a3))) + (a1 * a4) by VECTSP_1:8
.= ((- (a1 * a2)) - (a1 * a3)) + (a1 * a4) by VECTSP_1:8 ; :: thesis: a1 * (((- a2) - a3) - a4) = ((- (a1 * a2)) - (a1 * a3)) - (a1 * a4)
thus a1 * (((- a2) - a3) - a4) = (a1 * ((- a2) + (- a3))) + (a1 * (- a4)) by VECTSP_1:4
.= ((a1 * (- a2)) + (a1 * (- a3))) + (a1 * (- a4)) by VECTSP_1:4
.= ((- (a1 * a2)) + (a1 * (- a3))) + (a1 * (- a4)) by VECTSP_1:8
.= ((- (a1 * a2)) - (a1 * a3)) + (a1 * (- a4)) by VECTSP_1:8
.= ((- (a1 * a2)) - (a1 * a3)) - (a1 * a4) by VECTSP_1:8 ; :: thesis: verum