let L be non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for a being Element of L

for p, q being sequence of L holds a * (p + q) = (a * p) + (a * q)

let a be Element of L; :: thesis: for p, q being sequence of L holds a * (p + q) = (a * p) + (a * q)

let p, q be sequence of L; :: thesis: a * (p + q) = (a * p) + (a * q)

for i being Element of NAT holds (a * (p + q)) . i = ((a * p) + (a * q)) . i

for p, q being sequence of L holds a * (p + q) = (a * p) + (a * q)

let a be Element of L; :: thesis: for p, q being sequence of L holds a * (p + q) = (a * p) + (a * q)

let p, q be sequence of L; :: thesis: a * (p + q) = (a * p) + (a * q)

for i being Element of NAT holds (a * (p + q)) . i = ((a * p) + (a * q)) . i

proof

hence
a * (p + q) = (a * p) + (a * q)
by FUNCT_2:63; :: thesis: verum
let i be Element of NAT ; :: thesis: (a * (p + q)) . i = ((a * p) + (a * q)) . i

a * ((p + q) . i) = a * ((p . i) + (q . i)) by NORMSP_1:def 2

.= (a * (p . i)) + (a * (q . i)) by VECTSP_1:def 7

.= ((a * p) . i) + (a * (q . i)) by POLYNOM5:def 4

.= ((a * p) . i) + ((a * q) . i) by POLYNOM5:def 4

.= ((a * p) + (a * q)) . i by NORMSP_1:def 2 ;

hence (a * (p + q)) . i = ((a * p) + (a * q)) . i by POLYNOM5:def 4; :: thesis: verum

end;a * ((p + q) . i) = a * ((p . i) + (q . i)) by NORMSP_1:def 2

.= (a * (p . i)) + (a * (q . i)) by VECTSP_1:def 7

.= ((a * p) . i) + (a * (q . i)) by POLYNOM5:def 4

.= ((a * p) . i) + ((a * q) . i) by POLYNOM5:def 4

.= ((a * p) + (a * q)) . i by NORMSP_1:def 2 ;

hence (a * (p + q)) . i = ((a * p) + (a * q)) . i by POLYNOM5:def 4; :: thesis: verum