let n be Ordinal; :: thesis: for L being non empty right_add-cancelable right-distributive left_zeroed doubleLoopStr

for p being Series of n,L

for b being bag of n

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

let L be non empty right_add-cancelable right-distributive left_zeroed doubleLoopStr ; :: thesis: for p being Series of n,L

for b being bag of n

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

let p be Series of n,L; :: thesis: for b being bag of n

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

let b be bag of n; :: thesis: for a being Element of L holds b *' (a * p) = a * (b *' p)

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

set q1 = b *' (a * p);

set q2 = a * (b *' p);

.= dom (a * (b *' p)) by FUNCT_2:def 1 ;

hence b *' (a * p) = a * (b *' p) by A1, FUNCT_1:2; :: thesis: verum

for p being Series of n,L

for b being bag of n

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

let L be non empty right_add-cancelable right-distributive left_zeroed doubleLoopStr ; :: thesis: for p being Series of n,L

for b being bag of n

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

let p be Series of n,L; :: thesis: for b being bag of n

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

let b be bag of n; :: thesis: for a being Element of L holds b *' (a * p) = a * (b *' p)

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

set q1 = b *' (a * p);

set q2 = a * (b *' p);

A1: now :: thesis: for x being object st x in dom (b *' (a * p)) holds

(b *' (a * p)) . x = (a * (b *' p)) . x

dom (b *' (a * p)) =
Bags n
by FUNCT_2:def 1
(b *' (a * p)) . x = (a * (b *' p)) . x

let x be object ; :: thesis: ( x in dom (b *' (a * p)) implies (b *' (a * p)) . x = (a * (b *' p)) . x )

assume x in dom (b *' (a * p)) ; :: thesis: (b *' (a * p)) . x = (a * (b *' p)) . x

then reconsider u = x as bag of n ;

end;assume x in dom (b *' (a * p)) ; :: thesis: (b *' (a * p)) . x = (a * (b *' p)) . x

then reconsider u = x as bag of n ;

now :: thesis: ( ( b divides u & (b *' (a * p)) . u = (a * (b *' p)) . u ) or ( not b divides u & (b *' (a * p)) . u = (a * (b *' p)) . u ) )end;

hence
(b *' (a * p)) . x = (a * (b *' p)) . x
; :: thesis: verumper cases
( b divides u or not b divides u )
;

end;

.= dom (a * (b *' p)) by FUNCT_2:def 1 ;

hence b *' (a * p) = a * (b *' p) by A1, FUNCT_1:2; :: thesis: verum