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

for p being Series of n,L

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

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

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

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

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

for x being object st x in Bags n holds

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

for p being Series of n,L

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

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

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

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

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

for x being object st x in Bags n holds

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

proof

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

set cL = the carrier of L;

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

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

then reconsider b = x as bag of n ;

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

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

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

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

end;set cL = the carrier of L;

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

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

then reconsider b = x as bag of n ;

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

proof

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

consider s being FinSequence of the carrier of L such that

A2: ((a | (n,L)) *' p) . 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 = ((a | (n,L)) . b1) * (p . b2) ) by POLYNOM1:def 10;

not s is empty by A3;

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

A5: s1 = s . 1 and

A6: s = <*s1*> ^ t by FINSEQ_3:102;

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

then consider b1, b2 being bag of n such that

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

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

1 in dom s by A25, FINSEQ_5:6;

then A28: s /. 1 = s . 1 by PARTFUN1:def 6;

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

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

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

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

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

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

A2: ((a | (n,L)) *' p) . 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 = ((a | (n,L)) . b1) * (p . b2) ) by POLYNOM1:def 10;

not s is empty by A3;

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

A5: s1 = s . 1 and

A6: s = <*s1*> ^ t by FINSEQ_3:102;

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

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

A25:
not s is empty
by A3;per cases
( t = <*> the carrier of L or t <> <*> the carrier of L )
;

end;

suppose A9:
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 )

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

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

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

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

.= s . (k + 1) by A6, A11, FINSEQ_3:103 ;

1 <= k by A11, FINSEQ_3:25;

then A13: 1 < k + 1 by NAT_1:13;

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

then A14: k + 1 <= len s by A10, XREAL_1:6;

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

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

then A17: s /. (k + 1) = s . (k + 1) by A15, PARTFUN1:def 6;

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

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

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

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

.= s . (k + 1) by A6, A11, FINSEQ_3:103 ;

1 <= k by A11, FINSEQ_3:25;

then A13: 1 < k + 1 by NAT_1:13;

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

then A14: k + 1 <= len s by A10, XREAL_1:6;

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

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

then A17: s /. (k + 1) = s . (k + 1) by A15, PARTFUN1:def 6;

per cases
( k + 1 < len s or k + 1 = len s )
by A14, XXREAL_0:1;

end;

suppose A18:
k + 1 < len s
; :: 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

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

A20: s /. (k1 + 1) = ((a | (n,L)) . b1) * (p . b2) by A4, A16, A15;

b1 <> EmptyBag n by A3, A13, A18, A19, PRE_POLY:72;

hence t /. k = (0. L) * (p . b2) by A12, A17, A20, Th18

.= 0. L ;

:: thesis: verum

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

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

A20: s /. (k1 + 1) = ((a | (n,L)) . b1) * (p . b2) by A4, A16, A15;

b1 <> EmptyBag n by A3, A13, A18, A19, PRE_POLY:72;

hence t /. k = (0. L) * (p . b2) by A12, A17, A20, Th18

.= 0. L ;

:: thesis: verum

suppose A21:
k + 1 = len s
; :: thesis: t /. b_{1} = 0. L

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

A24: s /. (k + 1) = ((a | (n,L)) . b1) * (p . b2) by A4, A16, A15;

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

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

then s . (k + 1) = (0. L) * (p . (EmptyBag n)) by A17, A24, A22, Th18

.= 0. L ;

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

end;

A22: 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, A10, FINSEQ_1:39;

hence contradiction by A9; :: thesis: verum

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

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

hence contradiction by A9; :: thesis: verum

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

A24: s /. (k + 1) = ((a | (n,L)) . b1) * (p . b2) by A4, A16, A15;

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

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

then s . (k + 1) = (0. L) * (p . (EmptyBag n)) by A17, A24, A22, Th18

.= 0. L ;

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

then consider b1, b2 being bag of n such that

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

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

1 in dom s by A25, FINSEQ_5:6;

then A28: s /. 1 = s . 1 by PARTFUN1:def 6;

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

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

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

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

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

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

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

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