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)

now

let 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 Def11;
consider r2 being FinSequence of the carrier of L such that
A4: len r2 = i + 1 and
A5: (p *' q) . i = Sum r2 and
A6: for k being Element of NAT st k in dom r2 holds
r2 . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by Def11;
consider r3 being FinSequence of the carrier of L such that
A7: len r3 = i + 1 and
A8: (p *' r) . i = Sum r3 and
A9: for k being Element of NAT st k in dom r3 holds
r3 . k = (p . (k -' 1)) * (r . ((i + 1) -' k)) by Def11;
reconsider r2' = r2, r3' = r3 as Element of (i + 1) -tuples_on the carrier of L by A4, A7, FINSEQ_2:110;
A10: len (r2' + r3') = i + 1 by FINSEQ_1:def 18;
X: dom r1 = Seg (i + 1) by A1, FINSEQ_1:def 3;

now

let k be Nat; :: thesis: ( k in dom r1 implies r1 . k = (r2 + r3) . k )
assume k in dom r1 ; :: thesis: r1 . k = (r2 + r3) . k
then A11: ( k in dom r1 & k in dom r2 & k in dom r3 & k in dom (r2 + r3) ) by A4, A7, A10, X, FINSEQ_1:def 3;
then A12: r2 . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by A6;
A13: r3 . k = (p . (k -' 1)) * (r . ((i + 1) -' k)) by A9, A11;
thus r1 . k = (p . (k -' 1)) * ((q + r) . ((i + 1) -' k)) by A3, A11
.= (p . (k -' 1)) * ((q . ((i + 1) -' k)) + (r . ((i + 1) -' k))) by NORMSP_1:def 5
.= ((p . (k -' 1)) * (q . ((i + 1) -' k))) + ((p . (k -' 1)) * (r . ((i + 1) -' k))) by VECTSP_1:def 11
.= (r2 + r3) . k by A11, A12, A13, FVSUM_1:21 ; :: thesis: verum

end;

then Sum r1 = Sum (r2' + r3') by A1, A10, FINSEQ_2:10
.= (Sum r2) + (Sum r3) by FVSUM_1:95 ;
hence (p *' (q + r)) . i = ((p *' q) + (p *' r)) . i by A2, A5, A8, NORMSP_1:def 5; :: thesis: verum

end;

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