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

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

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

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

hence
p *' (q + r) = (p *' q) + (p *' r)
; :: thesis: verumlet i be Element of NAT ; :: thesis: (p *' (q + r)) . i = ((p *' q) + (p *' 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 . (k -' 1)) * ((q + 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: (p *' r) . i = Sum r3 and

A7: for k being Element of NAT st k in dom r3 holds

r3 . k = (p . (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 *' q) . i = Sum r2 and

A10: for k being Element of NAT st k in dom r2 holds

r2 . k = (p . (k -' 1)) * (q . ((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 *' q) + (p *' 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 . (k -' 1)) * ((q + 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: (p *' r) . i = Sum r3 and

A7: for k being Element of NAT st k in dom r3 holds

r3 . k = (p . (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 *' q) . i = Sum r2 and

A10: for k being Element of NAT st k in dom r2 holds

r2 . k = (p . (k -' 1)) * (q . ((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 = (p . (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)) * (q . ((i + 1) -' k)) by A10;

thus r1 . k = (p . (k -' 1)) * ((q + r) . ((i + 1) -' k)) by A3, A12

.= (p . (k -' 1)) * ((q . ((i + 1) -' k)) + (r . ((i + 1) -' k))) by NORMSP_1:def 2

.= ((p . (k -' 1)) * (q . ((i + 1) -' k))) + ((p . (k -' 1)) * (r . ((i + 1) -' k))) by VECTSP_1:def 2

.= (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 = (p . (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)) * (q . ((i + 1) -' k)) by A10;

thus r1 . k = (p . (k -' 1)) * ((q + r) . ((i + 1) -' k)) by A3, A12

.= (p . (k -' 1)) * ((q . ((i + 1) -' k)) + (r . ((i + 1) -' k))) by NORMSP_1:def 2

.= ((p . (k -' 1)) * (q . ((i + 1) -' k))) + ((p . (k -' 1)) * (r . ((i + 1) -' k))) by VECTSP_1:def 2

.= (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 *' q) + (p *' r)) . i by A2, A9, A6, NORMSP_1:def 2; :: thesis: verum