let i be Nat; :: thesis: for x being object
for n being Ordinal
for L being non trivial well-unital doubleLoopStr
for y being Function of n,L st x in n holds
eval (((EmptyBag n) +* (x,i)),y) = (power L) . ((y . x),i)
let x be object ; :: thesis: for n being Ordinal
for L being non trivial well-unital doubleLoopStr
for y being Function of n,L st x in n holds
eval (((EmptyBag n) +* (x,i)),y) = (power L) . ((y . x),i)
let n be Ordinal; :: thesis: for L being non trivial well-unital doubleLoopStr
for y being Function of n,L st x in n holds
eval (((EmptyBag n) +* (x,i)),y) = (power L) . ((y . x),i)
let L be non trivial well-unital doubleLoopStr ; :: thesis: for y being Function of n,L st x in n holds
eval (((EmptyBag n) +* (x,i)),y) = (power L) . ((y . x),i)
let y be Function of n,L; :: thesis: ( x in n implies eval (((EmptyBag n) +* (x,i)),y) = (power L) . ((y . x),i) )
assume A1: x in n ; :: thesis: eval (((EmptyBag n) +* (x,i)),y) = (power L) . ((y . x),i)
A2: n = dom y by PARTFUN1:def 2;
reconsider x = x as set by TARSKI:1;
set E = EmptyBag n;
set Ex = (EmptyBag n) +* (x,i);

per cases ( i <> 0 or i = 0 ) ;

suppose A3: i <> 0 ; :: thesis: eval (((EmptyBag n) +* (x,i)),y) = (power L) . ((y . x),i)

A4: dom (EmptyBag n) = n by PARTFUN1:def 2;
support ((EmptyBag n) +* (x,i)) = {x} by Th13, A1, A3;
then eval (((EmptyBag n) +* (x,i)),y) = (power L) . ((y . x),(((EmptyBag n) +* (x,i)) . x)) by POLYNOM2:15;
hence eval (((EmptyBag n) +* (x,i)),y) = (power L) . ((y . x),i) by A4, A1, FUNCT_7:31; :: thesis: verum

end;

suppose A5: i = 0 ; :: thesis: eval (((EmptyBag n) +* (x,i)),y) = (power L) . ((y . x),i)

then ( EmptyBag n = (EmptyBag n) +* (x,((EmptyBag n) . x)) & (EmptyBag n) . x = i ) by FUNCT_7:35;
then eval (((EmptyBag n) +* (x,i)),y) = 1_ L by POLYNOM2:14
.= (power L) . ((y /. x),i) by A5, GROUP_1:def 7 ;
hence eval (((EmptyBag n) +* (x,i)),y) = (power L) . ((y . x),i) by A2, A1, PARTFUN1:def 6; :: thesis: verum

end;

end;