let L be non empty right_complementable Abelian add-associative right_zeroed left-distributive doubleLoopStr ; :: thesis: for p, q, r being sequence of L holds (p + q) *' r = (p *' r) + (q *' r)
let p, q, r be sequence of L; :: thesis: (p + q) *' r = (p *' r) + (q *' r)

now :: thesis: for i being Element of NAT holds ((p + q) *' r) . i = ((p *' r) + (q *' r)) . i

let i be Element of NAT ; :: thesis: ((p + q) *' r) . i = ((p *' r) + (q *' r)) . i
consider r1 being FinSequence of the carrier of L such that
A1: len r1 = i + 1 and
A2: ((p + q) *' r) . i = Sum r1 and
A3: for k being Element of NAT st k in dom r1 holds
r1 . k = ((p + q) . (k -' 1)) * (r . ((i + 1) -' k)) by Def9;
A4: dom r1 = Seg (i + 1) by A1, FINSEQ_1:def 3;
consider r3 being FinSequence of the carrier of L such that
A5: len r3 = i + 1 and
A6: (q *' r) . i = Sum r3 and
A7: for k being Element of NAT st k in dom r3 holds
r3 . k = (q . (k -' 1)) * (r . ((i + 1) -' k)) by Def9;
consider r2 being FinSequence of the carrier of L such that
A8: len r2 = i + 1 and
A9: (p *' r) . i = Sum r2 and
A10: for k being Element of NAT st k in dom r2 holds
r2 . k = (p . (k -' 1)) * (r . ((i + 1) -' k)) by Def9;
reconsider r29 = r2, r39 = r3 as Element of (i + 1) -tuples_on the carrier of L by A8, A5, FINSEQ_2:92;
A11: len (r29 + r39) = i + 1 by CARD_1:def 7;

now :: thesis: for k being Nat st k in dom r1 holds
r1 . k = (r2 + r3) . k

let k be Nat; :: thesis: ( k in dom r1 implies r1 . k = (r2 + r3) . k )
assume A12: k in dom r1 ; :: thesis: r1 . k = (r2 + r3) . k
then A13: k in dom (r2 + r3) by A11, A4, FINSEQ_1:def 3;
k in dom r3 by A5, A4, A12, FINSEQ_1:def 3;
then A14: r3 . k = (q . (k -' 1)) * (r . ((i + 1) -' k)) by A7;
k in dom r2 by A8, A4, A12, FINSEQ_1:def 3;
then A15: r2 . k = (p . (k -' 1)) * (r . ((i + 1) -' k)) by A10;
thus r1 . k = ((p + q) . (k -' 1)) * (r . ((i + 1) -' k)) by A3, A12
.= ((p . (k -' 1)) + (q . (k -' 1))) * (r . ((i + 1) -' k)) by NORMSP_1:def 2
.= ((p . (k -' 1)) * (r . ((i + 1) -' k))) + ((q . (k -' 1)) * (r . ((i + 1) -' k))) by VECTSP_1:def 3
.= (r2 + r3) . k by A13, A15, A14, FVSUM_1:17 ; :: thesis: verum

end;

then Sum r1 = Sum (r29 + r39) by A1, A11, FINSEQ_2:9
.= (Sum r2) + (Sum r3) by FVSUM_1:76 ;
hence ((p + q) *' r) . i = ((p *' r) + (q *' r)) . i by A2, A9, A6, NORMSP_1:def 2; :: thesis: verum

end;

hence (p + q) *' r = (p *' r) + (q *' r) ; :: thesis: verum