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 :: thesis: for i being Element of NAT holds (p *' (q + r)) . i = ((p *' q) + (p *' r)) . i
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 Def9;
A4: dom r1 = Seg (i + 1) by ;
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 ;
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 ;
k in dom r3 by ;
then A14: r3 . k = (p . (k -' 1)) * (r . ((i + 1) -' k)) by A7;
k in dom r2 by ;
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
.= (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 ; :: thesis: verum
end;
then Sum r1 = Sum (r29 + r39) by
.= (Sum r2) + (Sum r3) by FVSUM_1:76 ;
hence (p *' (q + r)) . i = ((p *' q) + (p *' r)) . i by ; :: thesis: verum
end;
hence p *' (q + r) = (p *' q) + (p *' r) ; :: thesis: verum