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);
A1: now :: thesis: for x being object st x in dom (b *' (a * p)) holds
(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 ;
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 ) )
per cases ( b divides u or not b divides u ) ;
case A2: b divides u ; :: thesis: (b *' (a * p)) . u = (a * (b *' p)) . u
hence (b *' (a * p)) . u = (a * p) . (u -' b) by POLYRED:def 1
.= a * (p . (u -' b)) by POLYNOM7:def 9
.= a * ((b *' p) . u) by A2, POLYRED:def 1
.= (a * (b *' p)) . u by POLYNOM7:def 9 ;
:: thesis: verum
end;
case A3: not b divides u ; :: thesis: (b *' (a * p)) . u = (a * (b *' p)) . u
hence (b *' (a * p)) . u = 0. L by POLYRED:def 1
.= a * (0. L) by BINOM:2
.= a * ((b *' p) . u) by A3, POLYRED:def 1
.= (a * (b *' p)) . u by POLYNOM7:def 9 ;
:: thesis: verum
end;
end;
end;
hence (b *' (a * p)) . x = (a * (b *' p)) . x ; :: thesis: verum
end;
dom (b *' (a * p)) = Bags n by FUNCT_2:def 1
.= dom (a * (b *' p)) by FUNCT_2:def 1 ;
hence b *' (a * p) = a * (b *' p) by A1, FUNCT_1:2; :: thesis: verum