let L be non empty right_complementable left_zeroed distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for a being Element of L

for p, q being sequence of L holds a * (p *' q) = (a * p) *' q

let a be Element of L; :: thesis: for p, q being sequence of L holds a * (p *' q) = (a * p) *' q

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

for x being Element of NAT holds (a * (p *' q)) . x = ((a * p) *' q) . x

for p, q being sequence of L holds a * (p *' q) = (a * p) *' q

let a be Element of L; :: thesis: for p, q being sequence of L holds a * (p *' q) = (a * p) *' q

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

for x being Element of NAT holds (a * (p *' q)) . x = ((a * p) *' q) . x

proof

hence
a * (p *' q) = (a * p) *' q
by FUNCT_2:63; :: thesis: verum
let i be Element of NAT ; :: thesis: (a * (p *' q)) . i = ((a * p) *' q) . i

consider f1 being FinSequence of the carrier of L such that

A1: len f1 = i + 1 and

A2: (p *' q) . i = Sum f1 and

A3: for k being Element of NAT st k in dom f1 holds

f1 . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by POLYNOM3:def 9;

consider f2 being FinSequence of the carrier of L such that

A4: len f2 = i + 1 and

A5: ((a * p) *' q) . i = Sum f2 and

A6: for k being Element of NAT st k in dom f2 holds

f2 . k = ((a * p) . (k -' 1)) * (q . ((i + 1) -' k)) by POLYNOM3:def 9;

A7: dom (a * f1) = dom f1 by POLYNOM1:def 1

.= dom f2 by A1, A4, FINSEQ_3:29 ;

A8: for k being Nat st k in dom f2 holds

f2 . k = (a * f1) . k

.= Sum (a * f1) by BINOM:4

.= ((a * p) *' q) . i by A5, A7, A8, FINSEQ_1:13 ; :: thesis: verum

end;consider f1 being FinSequence of the carrier of L such that

A1: len f1 = i + 1 and

A2: (p *' q) . i = Sum f1 and

A3: for k being Element of NAT st k in dom f1 holds

f1 . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by POLYNOM3:def 9;

consider f2 being FinSequence of the carrier of L such that

A4: len f2 = i + 1 and

A5: ((a * p) *' q) . i = Sum f2 and

A6: for k being Element of NAT st k in dom f2 holds

f2 . k = ((a * p) . (k -' 1)) * (q . ((i + 1) -' k)) by POLYNOM3:def 9;

A7: dom (a * f1) = dom f1 by POLYNOM1:def 1

.= dom f2 by A1, A4, FINSEQ_3:29 ;

A8: for k being Nat st k in dom f2 holds

f2 . k = (a * f1) . k

proof

thus (a * (p *' q)) . i =
a * (Sum f1)
by A2, POLYNOM5:def 4
let k be Nat; :: thesis: ( k in dom f2 implies f2 . k = (a * f1) . k )

assume A9: k in dom f2 ; :: thesis: f2 . k = (a * f1) . k

A10: k in dom f1 by A1, A4, A9, FINSEQ_3:29;

then A11: (p . (k -' 1)) * (q . ((i + 1) -' k)) = f1 . k by A3

.= f1 /. k by A10, PARTFUN1:def 6 ;

thus f2 . k = ((a * p) . (k -' 1)) * (q . ((i + 1) -' k)) by A6, A9

.= (a * (p . (k -' 1))) * (q . ((i + 1) -' k)) by POLYNOM5:def 4

.= a * (f1 /. k) by A11, GROUP_1:def 3

.= (a * f1) /. k by A10, POLYNOM1:def 1

.= (a * f1) . k by A7, A9, PARTFUN1:def 6 ; :: thesis: verum

end;assume A9: k in dom f2 ; :: thesis: f2 . k = (a * f1) . k

A10: k in dom f1 by A1, A4, A9, FINSEQ_3:29;

then A11: (p . (k -' 1)) * (q . ((i + 1) -' k)) = f1 . k by A3

.= f1 /. k by A10, PARTFUN1:def 6 ;

thus f2 . k = ((a * p) . (k -' 1)) * (q . ((i + 1) -' k)) by A6, A9

.= (a * (p . (k -' 1))) * (q . ((i + 1) -' k)) by POLYNOM5:def 4

.= a * (f1 /. k) by A11, GROUP_1:def 3

.= (a * f1) /. k by A10, POLYNOM1:def 1

.= (a * f1) . k by A7, A9, PARTFUN1:def 6 ; :: thesis: verum

.= Sum (a * f1) by BINOM:4

.= ((a * p) *' q) . i by A5, A7, A8, FINSEQ_1:13 ; :: thesis: verum