let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for b being bag of the carrier of L

for f being FinSequence of the carrier of (Polynom-Ring L) *

for s being FinSequence of L st len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds

f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) holds

len (FlattenSeq f) = degree b

let b be bag of the carrier of L; :: thesis: for f being FinSequence of the carrier of (Polynom-Ring L) *

for s being FinSequence of L st len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds

f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) holds

len (FlattenSeq f) = degree b

let f be FinSequence of the carrier of (Polynom-Ring L) * ; :: thesis: for s being FinSequence of L st len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds

f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) holds

len (FlattenSeq f) = degree b

let s be FinSequence of L; :: thesis: ( len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds

f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) implies len (FlattenSeq f) = degree b )

assume that

A1: len f = card (support b) and

A2: s = canFS (support b) and

A3: for i being Element of NAT st i in dom f holds

f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ; :: thesis: len (FlattenSeq f) = degree b

reconsider Cf = Card f as FinSequence of NAT ;

consider g being FinSequence of NAT such that

A4: degree b = Sum g and

A5: g = b * (canFS (support b)) by Def3;

len s = card (support b) by A2, FINSEQ_1:93;

then A6: dom f = dom s by A1, FINSEQ_3:29;

hence len (FlattenSeq f) = degree b by A4, A7, FINSEQ_1:13; :: thesis: verum

for f being FinSequence of the carrier of (Polynom-Ring L) *

for s being FinSequence of L st len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds

f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) holds

len (FlattenSeq f) = degree b

let b be bag of the carrier of L; :: thesis: for f being FinSequence of the carrier of (Polynom-Ring L) *

for s being FinSequence of L st len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds

f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) holds

len (FlattenSeq f) = degree b

let f be FinSequence of the carrier of (Polynom-Ring L) * ; :: thesis: for s being FinSequence of L st len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds

f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) holds

len (FlattenSeq f) = degree b

let s be FinSequence of L; :: thesis: ( len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds

f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) implies len (FlattenSeq f) = degree b )

assume that

A1: len f = card (support b) and

A2: s = canFS (support b) and

A3: for i being Element of NAT st i in dom f holds

f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ; :: thesis: len (FlattenSeq f) = degree b

reconsider Cf = Card f as FinSequence of NAT ;

consider g being FinSequence of NAT such that

A4: degree b = Sum g and

A5: g = b * (canFS (support b)) by Def3;

len s = card (support b) by A2, FINSEQ_1:93;

then A6: dom f = dom s by A1, FINSEQ_3:29;

A7: now :: thesis: ( dom (Card f) = dom g & ( for i being Nat st i in dom (Card f) holds

Cf . i = g . i ) )

len (FlattenSeq f) = Sum Cf
by PRE_POLY:27;Cf . i = g . i ) )

A8:
rng s c= dom b

.= dom g by A2, A6, A5, A8, RELAT_1:27 ; :: thesis: for i being Nat st i in dom (Card f) holds

Cf . i = g . i

let i be Nat; :: thesis: ( i in dom (Card f) implies Cf . i = g . i )

assume i in dom (Card f) ; :: thesis: Cf . i = g . i

then A10: i in dom f by CARD_3:def 2;

then A11: g . i = b . (s . i) by A2, A6, A5, FUNCT_1:13;

f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) by A3, A10;

then A12: len (f . i) = b . (s /. i) by Def9;

thus Cf . i = card (f . i) by A10, CARD_3:def 2

.= g . i by A6, A10, A12, A11, PARTFUN1:def 6 ; :: thesis: verum

end;proof

thus dom (Card f) =
dom f
by CARD_3:def 2
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng s or x in dom b )

assume x in rng s ; :: thesis: x in dom b

then A9: x in support b by A2, FUNCT_2:def 3;

support b c= dom b by PRE_POLY:37;

hence x in dom b by A9; :: thesis: verum

end;assume x in rng s ; :: thesis: x in dom b

then A9: x in support b by A2, FUNCT_2:def 3;

support b c= dom b by PRE_POLY:37;

hence x in dom b by A9; :: thesis: verum

.= dom g by A2, A6, A5, A8, RELAT_1:27 ; :: thesis: for i being Nat st i in dom (Card f) holds

Cf . i = g . i

let i be Nat; :: thesis: ( i in dom (Card f) implies Cf . i = g . i )

assume i in dom (Card f) ; :: thesis: Cf . i = g . i

then A10: i in dom f by CARD_3:def 2;

then A11: g . i = b . (s . i) by A2, A6, A5, FUNCT_1:13;

f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) by A3, A10;

then A12: len (f . i) = b . (s /. i) by Def9;

thus Cf . i = card (f . i) by A10, CARD_3:def 2

.= g . i by A6, A10, A12, A11, PARTFUN1:def 6 ; :: thesis: verum

hence len (FlattenSeq f) = degree b by A4, A7, FINSEQ_1:13; :: thesis: verum