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;

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

A8: rng s c= dom b

proof

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;

thus dom (Card f) = dom f by CARD_3:def 2
.= 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;

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