let L be non empty right_complementable Abelian add-associative right_zeroed right-distributive doubleLoopStr ; for p, q, r being sequence of L holds p *' (q + r) = (p *' q) + (p *' r)
let p, q, r be sequence of L; p *' (q + r) = (p *' q) + (p *' r)
now for i being Element of NAT holds (p *' (q + r)) . i = ((p *' q) + (p *' r)) . ilet i be
Element of
NAT ;
(p *' (q + r)) . i = ((p *' q) + (p *' r)) . iconsider 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 for k being Nat st k in dom r1 holds
r1 . k = (r2 + r3) . klet k be
Nat;
( k in dom r1 implies r1 . k = (r2 + r3) . k )assume A12:
k in dom r1
;
r1 . k = (r2 + r3) . kthen 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
;
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 *' q) + (p *' r)) . i
by A2, A9, A6, NORMSP_1:def 2;
verum end;
hence
p *' (q + r) = (p *' q) + (p *' r)
; verum