let L be non empty associative doubleLoopStr ; :: thesis: for a, b being Element of L

for p being sequence of L holds (a * b) * p = a * (b * p)

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

let p be sequence of L; :: thesis: (a * b) * p = a * (b * p)

for i being Element of NAT holds ((a * b) * p) . i = (a * (b * p)) . i

for p being sequence of L holds (a * b) * p = a * (b * p)

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

let p be sequence of L; :: thesis: (a * b) * p = a * (b * p)

for i being Element of NAT holds ((a * b) * p) . i = (a * (b * p)) . i

proof

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

thus ((a * b) * p) . i = (a * b) * (p . i) by POLYNOM5:def 4

.= a * (b * (p . i)) by GROUP_1:def 3

.= a * ((b * p) . i) by POLYNOM5:def 4

.= (a * (b * p)) . i by POLYNOM5:def 4 ; :: thesis: verum

end;thus ((a * b) * p) . i = (a * b) * (p . i) by POLYNOM5:def 4

.= a * (b * (p . i)) by GROUP_1:def 3

.= a * ((b * p) . i) by POLYNOM5:def 4

.= (a * (b * p)) . i by POLYNOM5:def 4 ; :: thesis: verum