let n be Ordinal; :: thesis: for L being non trivial associative commutative well-unital doubleLoopStr
for x being Function of n,L
for b being bag of n
for S being one-to-one FinSequence of n st rng S = support b holds
ex y being FinSequence of L st
( len y = card (support b) & eval (b,x) = Product y & ( for i being Nat st 1 <= i & i <= len y holds
y /. i = (power L) . (((x * S) /. i),((b * S) /. i)) ) )
let L be non trivial associative commutative well-unital doubleLoopStr ; :: thesis: for x being Function of n,L
for b being bag of n
for S being one-to-one FinSequence of n st rng S = support b holds
ex y being FinSequence of L st
( len y = card (support b) & eval (b,x) = Product y & ( for i being Nat st 1 <= i & i <= len y holds
y /. i = (power L) . (((x * S) /. i),((b * S) /. i)) ) )
let x be Function of n,L; :: thesis: for b being bag of n
for S being one-to-one FinSequence of n st rng S = support b holds
ex y being FinSequence of L st
( len y = card (support b) & eval (b,x) = Product y & ( for i being Nat st 1 <= i & i <= len y holds
y /. i = (power L) . (((x * S) /. i),((b * S) /. i)) ) )
let b be bag of n; :: thesis: for S being one-to-one FinSequence of n st rng S = support b holds
ex y being FinSequence of L st
( len y = card (support b) & eval (b,x) = Product y & ( for i being Nat st 1 <= i & i <= len y holds
y /. i = (power L) . (((x * S) /. i),((b * S) /. i)) ) )
let S be one-to-one FinSequence of n; :: thesis: ( rng S = support b implies ex y being FinSequence of L st
( len y = card (support b) & eval (b,x) = Product y & ( for i being Nat st 1 <= i & i <= len y holds
y /. i = (power L) . (((x * S) /. i),((b * S) /. i)) ) ) )
assume A1: rng S = support b ; :: thesis: ex y being FinSequence of L st
( len y = card (support b) & eval (b,x) = Product y & ( for i being Nat st 1 <= i & i <= len y holds
y /. i = (power L) . (((x * S) /. i),((b * S) /. i)) ) )
set SG = SgmX ((RelIncl n),(support b));
consider y being FinSequence of L such that
A2: ( len y = len (SgmX ((RelIncl n),(support b))) & eval (b,x) = Product y ) and
A3: for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = (power L) . (((x * (SgmX ((RelIncl n),(support b)))) /. i),((b * (SgmX ((RelIncl n),(support b)))) /. i)) by POLYNOM2:def 2;
A4: RelIncl n linearly_orders support b by PRE_POLY:82;
A5: ( SgmX ((RelIncl n),(support b)) is one-to-one & len (SgmX ((RelIncl n),(support b))) = card (support b) ) by PRE_POLY:10, PRE_POLY:11, PRE_POLY:82;
A6: rng (SgmX ((RelIncl n),(support b))) = support b by A4, PRE_POLY:def 2;
then consider H being Function such that
A7: ( dom H = dom S & rng H = dom (SgmX ((RelIncl n),(support b))) & H is one-to-one & (SgmX ((RelIncl n),(support b))) * H = S ) by A1, A5, RFINSEQ:26, CLASSES1:77;
A8: len S = len (SgmX ((RelIncl n),(support b))) by A1, A5, A6, FINSEQ_1:48;
A9: ( dom y = dom (SgmX ((RelIncl n),(support b))) & dom (SgmX ((RelIncl n),(support b))) = 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;
take yH ; :: thesis: ( len yH = card (support b) & eval (b,x) = Product yH & ( for i being Nat st 1 <= i & i <= len yH holds
yH /. i = (power L) . (((x * S) /. i),((b * S) /. i)) ) )
thus len yH = card (support b) by A7, A10, FINSEQ_3:29, A8, A5; :: thesis: ( eval (b,x) = Product yH & ( for i being Nat st 1 <= i & i <= len yH holds
yH /. i = (power L) . (((x * S) /. i),((b * S) /. i)) ) )
A12: H is Permutation of (dom y) ;
thus eval (b,x) = the multF of L "**" y by GROUP_4:def 2, A2
.= the multF of L "**" yH by FINSOP_1:7, A12
.= Product yH by GROUP_4:def 2 ; :: thesis: for i being Nat st 1 <= i & i <= len yH holds
yH /. i = (power L) . (((x * S) /. i),((b * S) /. i))
let i be Nat; :: thesis: ( 1 <= i & i <= len yH implies yH /. i = (power L) . (((x * S) /. i),((b * S) /. i)) )
assume A13: ( 1 <= i & i <= len yH ) ; :: thesis: yH /. i = (power L) . (((x * S) /. i),((b * S) /. i))
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 x = n by FUNCT_2:def 1;
then ( rng (SgmX ((RelIncl n),(support b))) c= dom x & rng S c= dom x ) ;
then A16: ( dom (x * (SgmX ((RelIncl n),(support b)))) = dom (SgmX ((RelIncl n),(support b))) & dom (x * S) = dom S ) by RELAT_1:27;
then A17: (x * (SgmX ((RelIncl n),(support b)))) /. (H /. i) = (x * (SgmX ((RelIncl n),(support b)))) . (H /. i) by A14, A7, PARTFUN1:def 6
.= x . ((SgmX ((RelIncl n),(support b))) . (H /. i)) by A16, A14, A7, FUNCT_1:12
.= x . (((SgmX ((RelIncl n),(support b))) * H) . i) by A14, A13, FINSEQ_3:25, A7, A10, FUNCT_1:12
.= (x * S) . i by A7, A16, A13, FINSEQ_3:25, A10, FUNCT_1:12
.= (x * S) /. i by A7, A16, A13, FINSEQ_3:25, A10, PARTFUN1:def 6 ;
dom b = n by PARTFUN1:def 2;
then ( rng (SgmX ((RelIncl n),(support b))) c= dom b & rng S c= dom b ) ;
then A18: ( dom (b * (SgmX ((RelIncl n),(support b)))) = dom (SgmX ((RelIncl n),(support b))) & dom (b * S) = dom S ) by RELAT_1:27;
then (b * (SgmX ((RelIncl n),(support b)))) /. (H /. i) = (b * (SgmX ((RelIncl n),(support b)))) . (H /. i) by A14, A7, PARTFUN1:def 6
.= b . ((SgmX ((RelIncl n),(support b))) . (H /. i)) by A18, A14, A7, FUNCT_1:12
.= b . (((SgmX ((RelIncl n),(support b))) * H) . i) by A14, A13, FINSEQ_3:25, A7, A10, FUNCT_1:12
.= (b * S) . i by A7, A18, A13, FINSEQ_3:25, A10, FUNCT_1:12
.= (b * S) /. i by A7, A18, A13, FINSEQ_3:25, A10, PARTFUN1:def 6 ;
hence yH /. i = (power L) . (((x * S) /. i),((b * S) /. i)) by A3, A17, A14, A15; :: thesis: verum