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 () *
for s being FinSequence of L st len f = card () & s = canFS () & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) holds
len () = degree b

let b be bag of the carrier of L; :: thesis: for f being FinSequence of the carrier of () *
for s being FinSequence of L st len f = card () & s = canFS () & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) holds
len () = degree b

let f be FinSequence of the carrier of () * ; :: thesis: for s being FinSequence of L st len f = card () & s = canFS () & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) holds
len () = degree b

let s be FinSequence of L; :: thesis: ( len f = card () & s = canFS () & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) implies len () = degree b )

assume that
A1: len f = card () and
A2: s = canFS () 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 () = 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 ()) by Def3;
len s = card () by ;
then A6: dom f = dom s by ;
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 ;
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 ; :: 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 ;
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) by ;
then A12: len (f . i) = b . (s /. i) by Def9;
thus Cf . i = card (f . i) by
.= g . i by ; :: thesis: verum
end;
len () = Sum Cf by PRE_POLY:27;
hence len () = degree b by ; :: thesis: verum