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)

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

hence
(p + q) *' r = (p *' r) + (q *' r)
; :: thesis: verumlet 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;

.= (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;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

then Sum r1 =
Sum (r29 + r39)
by A1, A11, FINSEQ_2:9
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;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

.= (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