let x be object ; :: thesis: for n being Ordinal
for L being non trivial well-unital doubleLoopStr
for b being bag of n
for f being Function of n,L
for u being Element of L st b . x = 0 holds
eval (b,(f +* (x,u))) = eval (b,f)
let n be Ordinal; :: thesis: for L being non trivial well-unital doubleLoopStr
for b being bag of n
for f being Function of n,L
for u being Element of L st b . x = 0 holds
eval (b,(f +* (x,u))) = eval (b,f)
let L be non trivial well-unital doubleLoopStr ; :: thesis: for b being bag of n
for f being Function of n,L
for u being Element of L st b . x = 0 holds
eval (b,(f +* (x,u))) = eval (b,f)
let b be bag of n; :: thesis: for f being Function of n,L
for u being Element of L st b . x = 0 holds
eval (b,(f +* (x,u))) = eval (b,f)
let f be Function of n,L; :: thesis: for u being Element of L st b . x = 0 holds
eval (b,(f +* (x,u))) = eval (b,f)
let u be Element of L; :: thesis: ( b . x = 0 implies eval (b,(f +* (x,u))) = eval (b,f) )
assume A1: b . x = 0 ; :: thesis: eval (b,(f +* (x,u))) = eval (b,f)
set S = SgmX ((RelIncl n),(support b));
set fxu = f +* (x,u);
consider y being FinSequence of L such that
A2: ( len y = len (SgmX ((RelIncl n),(support b))) & eval (b,(f +* (x,u))) = Product y ) and
A3: for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = (power L) . ((((f +* (x,u)) * (SgmX ((RelIncl n),(support b)))) /. i),((b * (SgmX ((RelIncl n),(support b)))) /. i)) by POLYNOM2:def 2;
RelIncl n linearly_orders support b by PRE_POLY:82;
then A4: rng (SgmX ((RelIncl n),(support b))) = support b by PRE_POLY:def 2;
for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = (power L) . (((f * (SgmX ((RelIncl n),(support b)))) /. i),((b * (SgmX ((RelIncl n),(support b)))) /. i))

proof

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= len y implies y /. i = (power L) . (((f * (SgmX ((RelIncl n),(support b)))) /. i),((b * (SgmX ((RelIncl n),(support b)))) /. i)) )
assume A5: ( 1 <= i & i <= len y ) ; :: thesis: y /. i = (power L) . (((f * (SgmX ((RelIncl n),(support b)))) /. i),((b * (SgmX ((RelIncl n),(support b)))) /. i))
( dom f = n & n = dom (f +* (x,u)) ) by FUNCT_2:def 1;
then A6: ( dom (f * (SgmX ((RelIncl n),(support b)))) = dom (SgmX ((RelIncl n),(support b))) & dom (SgmX ((RelIncl n),(support b))) = dom ((f +* (x,u)) * (SgmX ((RelIncl n),(support b)))) ) by A4, RELAT_1:27;
then A7: ( (f * (SgmX ((RelIncl n),(support b)))) /. i = (f * (SgmX ((RelIncl n),(support b)))) . i & (f * (SgmX ((RelIncl n),(support b)))) . i = f . ((SgmX ((RelIncl n),(support b))) . i) & i in dom (SgmX ((RelIncl n),(support b))) ) by A5, FINSEQ_3:25, A2, PARTFUN1:def 6, FUNCT_1:12;
then (SgmX ((RelIncl n),(support b))) . i in rng (SgmX ((RelIncl n),(support b))) by FUNCT_1:def 3;
then A8: (SgmX ((RelIncl n),(support b))) . i <> x by A1, A4, PRE_POLY:def 7;
( ((f +* (x,u)) * (SgmX ((RelIncl n),(support b)))) /. i = ((f +* (x,u)) * (SgmX ((RelIncl n),(support b)))) . i & ((f +* (x,u)) * (SgmX ((RelIncl n),(support b)))) . i = (f +* (x,u)) . ((SgmX ((RelIncl n),(support b))) . i) ) by A6, A5, FINSEQ_3:25, A2, PARTFUN1:def 6, FUNCT_1:12;
then (f * (SgmX ((RelIncl n),(support b)))) /. i = ((f +* (x,u)) * (SgmX ((RelIncl n),(support b)))) /. i by A7, A8, FUNCT_7:32;
hence y /. i = (power L) . (((f * (SgmX ((RelIncl n),(support b)))) /. i),((b * (SgmX ((RelIncl n),(support b)))) /. i)) by A5, A3; :: thesis: verum

end;

hence eval (b,(f +* (x,u))) = eval (b,f) by A2, POLYNOM2:def 2; :: thesis: verum