let n be Ordinal; :: thesis: for L being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of n,L
for x being Function of n,L
for S being one-to-one FinSequence of Bags n st rng S = Support p holds
ex y being FinSequence of L st
( len y = card (Support p) & eval (p,x) = Sum y & ( for i being Nat st 1 <= i & i <= len y holds
y /. i = ((p * S) /. i) * (eval ((S /. i),x)) ) )
let L be non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for p being Polynomial of n,L
for x being Function of n,L
for S being one-to-one FinSequence of Bags n st rng S = Support p holds
ex y being FinSequence of L st
( len y = card (Support p) & eval (p,x) = Sum y & ( for i being Nat st 1 <= i & i <= len y holds
y /. i = ((p * S) /. i) * (eval ((S /. i),x)) ) )
let p be Polynomial of n,L; :: thesis: for x being Function of n,L
for S being one-to-one FinSequence of Bags n st rng S = Support p holds
ex y being FinSequence of L st
( len y = card (Support p) & eval (p,x) = Sum y & ( for i being Nat st 1 <= i & i <= len y holds
y /. i = ((p * S) /. i) * (eval ((S /. i),x)) ) )
let x be Function of n,L; :: thesis: for S being one-to-one FinSequence of Bags n st rng S = Support p holds
ex y being FinSequence of L st
( len y = card (Support p) & eval (p,x) = Sum y & ( for i being Nat st 1 <= i & i <= len y holds
y /. i = ((p * S) /. i) * (eval ((S /. i),x)) ) )
let S be one-to-one FinSequence of Bags n; :: thesis: ( rng S = Support p implies ex y being FinSequence of L st
( len y = card (Support p) & eval (p,x) = Sum y & ( for i being Nat st 1 <= i & i <= len y holds
y /. i = ((p * S) /. i) * (eval ((S /. i),x)) ) ) )
assume A1: rng S = Support p ; :: thesis: ex y being FinSequence of L st
( len y = card (Support p) & eval (p,x) = Sum y & ( for i being Nat st 1 <= i & i <= len y holds
y /. i = ((p * S) /. i) * (eval ((S /. i),x)) ) )
set SG = SgmX ((BagOrder n),(Support p));
consider y being FinSequence of L such that
A2: ( len y = len (SgmX ((BagOrder n),(Support p))) & eval (p,x) = Sum y ) and
A3: for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = ((p * (SgmX ((BagOrder n),(Support p)))) /. i) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x)) by POLYNOM2:def 4;
A4: BagOrder n linearly_orders Support p by POLYNOM2:18;
A5: ( SgmX ((BagOrder n),(Support p)) is one-to-one & len (SgmX ((BagOrder n),(Support p))) = card (Support p) ) by POLYNOM2:18, PRE_POLY:10, PRE_POLY:11;
A6: rng (SgmX ((BagOrder n),(Support p))) = Support p by A4, PRE_POLY:def 2;
then consider H being Function such that
A7: ( dom H = dom S & rng H = dom (SgmX ((BagOrder n),(Support p))) & H is one-to-one & (SgmX ((BagOrder n),(Support p))) * H = S ) by A1, A5, RFINSEQ:26, CLASSES1:77;
A8: len S = len (SgmX ((BagOrder n),(Support p))) by A1, A5, A6, FINSEQ_1:48;
A9: ( dom y = dom (SgmX ((BagOrder n),(Support p))) & dom (SgmX ((BagOrder n),(Support p))) = dom S ) by A2, A8, FINSEQ_3:29;
then A10: ( dom (y * H) = dom H & dom S = Seg (len S) ) by A7, RELAT_1:27, FINSEQ_1:def 3;
then reconsider yH = y * H as FinSequence by A7, FINSEQ_1:def 2;
reconsider H = H as Function of (dom y),(dom y) by A7, A9, FUNCT_2:1;
H is onto by A7, A2, FINSEQ_3:29;
then reconsider H = H as Permutation of (dom y) by A7;
A11: rng y c= the carrier of L ;
rng yH c= rng y by RELAT_1:26;
then rng yH c= the carrier of L by A11;
then reconsider yH = yH as FinSequence of L by FINSEQ_1:def 4;
reconsider yH = yH as FinSequence of L ;
take yH ; :: thesis: ( len yH = card (Support p) & eval (p,x) = Sum yH & ( for i being Nat st 1 <= i & i <= len yH holds
yH /. i = ((p * S) /. i) * (eval ((S /. i),x)) ) )
thus len yH = card (Support p) by A7, A10, FINSEQ_3:29, A8, A5; :: thesis: ( eval (p,x) = Sum yH & ( for i being Nat st 1 <= i & i <= len yH holds
yH /. i = ((p * S) /. i) * (eval ((S /. i),x)) ) )
A12: len y = len yH by A2, A8, A7, A10, FINSEQ_3:29;
for i being Nat st i in dom yH holds
yH . i = y . (H . i) by FUNCT_1:12;
hence eval (p,x) = Sum yH by A2, A12, RLVECT_2:6; :: thesis: for i being Nat st 1 <= i & i <= len yH holds
yH /. i = ((p * S) /. i) * (eval ((S /. i),x))
let i be Nat; :: thesis: ( 1 <= i & i <= len yH implies yH /. i = ((p * S) /. i) * (eval ((S /. i),x)) )
assume A13: ( 1 <= i & i <= len yH ) ; :: thesis: yH /. i = ((p * S) /. i) * (eval ((S /. i),x))
set Hi = H /. i;
i in dom yH by A13, FINSEQ_3:25;
then A14: ( yH /. i = yH . i & H . i = H /. i & yH . i = y . (H . i) & H . i in rng H ) by A10, PARTFUN1:def 6, FUNCT_1:12, FUNCT_1:def 3;
then A15: ( 1 <= H /. i & H /. i <= len y & H /. i in NAT & y . (H /. i) = y /. (H /. i) ) by FINSEQ_3:25, PARTFUN1:def 6;
dom p = Bags n by FUNCT_2:def 1;
then ( rng (SgmX ((BagOrder n),(Support p))) c= dom p & rng S c= dom p ) ;
then A16: ( dom (p * (SgmX ((BagOrder n),(Support p)))) = dom (SgmX ((BagOrder n),(Support p))) & dom (p * S) = dom S ) by RELAT_1:27;
then A17: (p * (SgmX ((BagOrder n),(Support p)))) /. (H /. i) = (p * (SgmX ((BagOrder n),(Support p)))) . (H /. i) by A14, A7, PARTFUN1:def 6
.= p . ((SgmX ((BagOrder n),(Support p))) . (H /. i)) by A16, A14, A7, FUNCT_1:12
.= p . (((SgmX ((BagOrder n),(Support p))) * H) . i) by A14, A13, FINSEQ_3:25, A7, A10, FUNCT_1:12
.= (p * S) . i by A7, A16, A13, FINSEQ_3:25, A10, FUNCT_1:12
.= (p * S) /. i by A7, A16, A13, FINSEQ_3:25, A10, PARTFUN1:def 6 ;
(SgmX ((BagOrder n),(Support p))) /. (H /. i) = (SgmX ((BagOrder n),(Support p))) . (H . i) by A14, A7, PARTFUN1:def 6
.= ((SgmX ((BagOrder n),(Support p))) * H) . i by A13, FINSEQ_3:25, A7, A10, FUNCT_1:12
.= S /. i by A13, FINSEQ_3:25, A7, A10, PARTFUN1:def 6 ;
hence yH /. i = ((p * S) /. i) * (eval ((S /. i),x)) by A3, A17, A14, A15; :: thesis: verum