let n be Ordinal; :: thesis: for L being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr

for p being Series of n,L

for a being Element of L holds p * a = p *' (a | (n,L))

let L be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ; :: thesis: for p being Series of n,L

for a being Element of L holds p * a = p *' (a | (n,L))

let p be Series of n,L; :: thesis: for a being Element of L holds p * a = p *' (a | (n,L))

let a be Element of L; :: thesis: p * a = p *' (a | (n,L))

for x being object st x in Bags n holds

(p * a) . x = (p *' (a | (n,L))) . x

for p being Series of n,L

for a being Element of L holds p * a = p *' (a | (n,L))

let L be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ; :: thesis: for p being Series of n,L

for a being Element of L holds p * a = p *' (a | (n,L))

let p be Series of n,L; :: thesis: for a being Element of L holds p * a = p *' (a | (n,L))

let a be Element of L; :: thesis: p * a = p *' (a | (n,L))

for x being object st x in Bags n holds

(p * a) . x = (p *' (a | (n,L))) . x

proof

hence
p * a = p *' (a | (n,L))
; :: thesis: verum
set O = a | (n,L);

set cL = the carrier of L;

let x be object ; :: thesis: ( x in Bags n implies (p * a) . x = (p *' (a | (n,L))) . x )

assume x in Bags n ; :: thesis: (p * a) . x = (p *' (a | (n,L))) . x

then reconsider b = x as bag of n ;

A1: for b being Element of Bags n holds (p *' (a | (n,L))) . b = (p . b) * a

then (p *' (a | (n,L))) . b = (p . b) * a by A1

.= (p * a) . b by Def10 ;

hence (p * a) . x = (p *' (a | (n,L))) . x ; :: thesis: verum

end;set cL = the carrier of L;

let x be object ; :: thesis: ( x in Bags n implies (p * a) . x = (p *' (a | (n,L))) . x )

assume x in Bags n ; :: thesis: (p * a) . x = (p *' (a | (n,L))) . x

then reconsider b = x as bag of n ;

A1: for b being Element of Bags n holds (p *' (a | (n,L))) . b = (p . b) * a

proof

b is Element of Bags n
by PRE_POLY:def 12;
let b be Element of Bags n; :: thesis: (p *' (a | (n,L))) . b = (p . b) * a

consider s being FinSequence of the carrier of L such that

A2: (p *' (a | (n,L))) . b = Sum s and

A3: len s = len (decomp b) and

A4: for k being Element of NAT st k in dom s holds

ex b1, b2 being bag of n st

( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * ((a | (n,L)) . b2) ) by POLYNOM1:def 10;

consider t being FinSequence of the carrier of L, s1 being Element of the carrier of L such that

A5: s = t ^ <*s1*> by A3, FINSEQ_2:19;

.= s1 by FINSEQ_1:42 ;

A24: Sum s = (Sum t) + (Sum <*s1*>) by A5, RLVECT_1:41;

not s is empty by A3;

then A25: len s in dom s by FINSEQ_5:6;

then consider b1, b2 being bag of n such that

A26: (decomp b) /. (len s) = <*b1,b2*> and

A27: s /. (len s) = (p . b1) * ((a | (n,L)) . b2) by A4;

A28: s /. (len s) = s . (len s) by A25, PARTFUN1:def 6;

(decomp b) /. (len s) = <*b,(EmptyBag n)*> by A3, PRE_POLY:71;

then A29: ( b1 = b & b2 = EmptyBag n ) by A26, FINSEQ_1:77;

Sum <*s1*> = s1 by RLVECT_1:44

.= (p . b) * a by A27, A29, A28, A23, Th18 ;

hence (p *' (a | (n,L))) . b = (p . b) * a by A2, A24, A6, RLVECT_1:4; :: thesis: verum

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

A2: (p *' (a | (n,L))) . b = Sum s and

A3: len s = len (decomp b) and

A4: for k being Element of NAT st k in dom s holds

ex b1, b2 being bag of n st

( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * ((a | (n,L)) . b2) ) by POLYNOM1:def 10;

consider t being FinSequence of the carrier of L, s1 being Element of the carrier of L such that

A5: s = t ^ <*s1*> by A3, FINSEQ_2:19;

A6: now :: thesis: Sum t = 0. Lend;

A23: s . (len s) =
(t ^ <*s1*>) . ((len t) + 1)
by A5, FINSEQ_2:16
per cases
( t = <*> the carrier of L or t <> <*> the carrier of L )
;

end;

suppose A7:
t <> <*> the carrier of L
; :: thesis: Sum t = 0. L

end;

now :: thesis: for k being Nat st k in dom t holds

t /. k = 0. L

hence
Sum t = 0. L
by MATRLIN:11; :: thesis: verumt /. k = 0. L

let k be Nat; :: thesis: ( k in dom t implies t /. b_{1} = 0. L )

A8: len s = (len t) + (len <*s1*>) by A5, FINSEQ_1:22

.= (len t) + 1 by FINSEQ_1:39 ;

assume A9: k in dom t ; :: thesis: t /. b_{1} = 0. L

then A10: t /. k = t . k by PARTFUN1:def 6

.= s . k by A5, A9, FINSEQ_1:def 7 ;

k <= len t by A9, FINSEQ_3:25;

then A11: k < len s by A8, NAT_1:13;

A12: 1 <= k by A9, FINSEQ_3:25;

then A13: k in dom (decomp b) by A3, A11, FINSEQ_3:25;

A14: dom s = dom (decomp b) by A3, FINSEQ_3:29;

then A15: s /. k = s . k by A13, PARTFUN1:def 6;

end;A8: len s = (len t) + (len <*s1*>) by A5, FINSEQ_1:22

.= (len t) + 1 by FINSEQ_1:39 ;

assume A9: k in dom t ; :: thesis: t /. b

then A10: t /. k = t . k by PARTFUN1:def 6

.= s . k by A5, A9, FINSEQ_1:def 7 ;

k <= len t by A9, FINSEQ_3:25;

then A11: k < len s by A8, NAT_1:13;

A12: 1 <= k by A9, FINSEQ_3:25;

then A13: k in dom (decomp b) by A3, A11, FINSEQ_3:25;

A14: dom s = dom (decomp b) by A3, FINSEQ_3:29;

then A15: s /. k = s . k by A13, PARTFUN1:def 6;

per cases
( 1 < k or k = 1 )
by A12, XXREAL_0:1;

end;

suppose A16:
1 < k
; :: thesis: t /. b_{1} = 0. L

reconsider k1 = k as Element of NAT by ORDINAL1:def 12;

consider b1, b2 being bag of n such that

A17: (decomp b) /. k1 = <*b1,b2*> and

A18: s /. k1 = (p . b1) * ((a | (n,L)) . b2) by A4, A14, A13;

b2 <> EmptyBag n by A3, A11, A16, A17, PRE_POLY:72;

hence t /. k = (p . b1) * (0. L) by A10, A15, A18, Th18

.= 0. L ;

:: thesis: verum

end;consider b1, b2 being bag of n such that

A17: (decomp b) /. k1 = <*b1,b2*> and

A18: s /. k1 = (p . b1) * ((a | (n,L)) . b2) by A4, A14, A13;

b2 <> EmptyBag n by A3, A11, A16, A17, PRE_POLY:72;

hence t /. k = (p . b1) * (0. L) by A10, A15, A18, Th18

.= 0. L ;

:: thesis: verum

suppose A19:
k = 1
; :: thesis: t /. b_{1} = 0. L

A21: (decomp b) /. k = <*b1,b2*> and

A22: s /. k = (p . b1) * ((a | (n,L)) . b2) by A4, A14, A13;

(decomp b) /. 1 = <*(EmptyBag n),b*> by PRE_POLY:71;

then ( b1 = EmptyBag n & b2 = b ) by A19, A21, FINSEQ_1:77;

then s . k = (p . (EmptyBag n)) * (0. L) by A15, A22, A20, Th18

.= 0. L ;

hence t /. k = 0. L by A10; :: thesis: verum

end;

A20: now :: thesis: not b = EmptyBag n

consider b1, b2 being bag of n such that assume
b = EmptyBag n
; :: thesis: contradiction

then decomp b = <*<*(EmptyBag n),(EmptyBag n)*>*> by PRE_POLY:73;

then (len t) + 1 = 0 + 1 by A3, A8, FINSEQ_1:39;

hence contradiction by A7; :: thesis: verum

end;then decomp b = <*<*(EmptyBag n),(EmptyBag n)*>*> by PRE_POLY:73;

then (len t) + 1 = 0 + 1 by A3, A8, FINSEQ_1:39;

hence contradiction by A7; :: thesis: verum

A21: (decomp b) /. k = <*b1,b2*> and

A22: s /. k = (p . b1) * ((a | (n,L)) . b2) by A4, A14, A13;

(decomp b) /. 1 = <*(EmptyBag n),b*> by PRE_POLY:71;

then ( b1 = EmptyBag n & b2 = b ) by A19, A21, FINSEQ_1:77;

then s . k = (p . (EmptyBag n)) * (0. L) by A15, A22, A20, Th18

.= 0. L ;

hence t /. k = 0. L by A10; :: thesis: verum

.= s1 by FINSEQ_1:42 ;

A24: Sum s = (Sum t) + (Sum <*s1*>) by A5, RLVECT_1:41;

not s is empty by A3;

then A25: len s in dom s by FINSEQ_5:6;

then consider b1, b2 being bag of n such that

A26: (decomp b) /. (len s) = <*b1,b2*> and

A27: s /. (len s) = (p . b1) * ((a | (n,L)) . b2) by A4;

A28: s /. (len s) = s . (len s) by A25, PARTFUN1:def 6;

(decomp b) /. (len s) = <*b,(EmptyBag n)*> by A3, PRE_POLY:71;

then A29: ( b1 = b & b2 = EmptyBag n ) by A26, FINSEQ_1:77;

Sum <*s1*> = s1 by RLVECT_1:44

.= (p . b) * a by A27, A29, A28, A23, Th18 ;

hence (p *' (a | (n,L))) . b = (p . b) * a by A2, A24, A6, RLVECT_1:4; :: thesis: verum

then (p *' (a | (n,L))) . b = (p . b) * a by A1

.= (p * a) . b by Def10 ;

hence (p * a) . x = (p *' (a | (n,L))) . x ; :: thesis: verum