let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for b being bag of
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 ; :: 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
len s = card (support b) by A2, Def1;
then A4: dom f = dom s by A1, FINSEQ_3:31;
reconsider Cf = Card f as FinSequence of NAT ;
A5: len (FlattenSeq f) = Sum Cf by POLYNOM1:30;
consider g being FinSequence of NAT such that
A6: degree b = Sum g and
A7: g = b * (canFS (support b)) by Def4;

now

A8: rng s c= dom b

proof

let x be set ; :: 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 POLYNOM1:41;
hence x in dom b by A9; :: thesis: verum

end;

thus dom (Card f) = dom f by CARD_3:def 2
.= dom g by A2, A4, A7, A8, RELAT_1:46 ; :: 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 A10: i in dom (Card f) ; :: thesis: Cf . i = g . i
A11: i in dom f by A10, CARD_3:def 2;
then f . i = fpoly_mult_root (s /. i),(b . (s /. i)) by A3;
then A12: len (f . i) = b . (s /. i) by Def10;
A13: g . i = b . (s . i) by A2, A4, A7, A11, FUNCT_1:23;
thus Cf . i = card (f . i) by A11, CARD_3:def 2
.= g . i by A4, A11, A12, A13, PARTFUN1:def 8 ; :: thesis: verum

end;

hence len (FlattenSeq f) = degree b by A5, A6, FINSEQ_1:17; :: thesis: verum