let n be Ordinal; :: thesis: for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for a being Element of L
for b being bag of n
for x being Function of n,L holds eval ((Monom (a,b)),x) = a * (eval (b,x))
let L be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for a being Element of L
for b being bag of n
for x being Function of n,L holds eval ((Monom (a,b)),x) = a * (eval (b,x))
let a be Element of L; :: thesis: for b being bag of n
for x being Function of n,L holds eval ((Monom (a,b)),x) = a * (eval (b,x))
let b be bag of n; :: thesis: for x being Function of n,L holds eval ((Monom (a,b)),x) = a * (eval (b,x))
let x be Function of n,L; :: thesis: eval ((Monom (a,b)),x) = a * (eval (b,x))
set m = Monom (a,b);

now :: thesis: ( ( a <> 0. L & eval ((Monom (a,b)),x) = a * (eval (b,x)) ) or ( a = 0. L & eval ((Monom (a,b)),x) = a * (eval (b,x)) ) )

per cases ( a <> 0. L or a = 0. L ) ;

case a <> 0. L ; :: thesis: eval ((Monom (a,b)),x) = a * (eval (b,x))

then A1: not a is zero ;
thus eval ((Monom (a,b)),x) = (coefficient (Monom (a,b))) * (eval ((term (Monom (a,b))),x)) by Th12
.= a * (eval ((term (Monom (a,b))),x)) by Th9
.= a * (eval (b,x)) by A1, Th10 ; :: thesis: verum

end;

case A2: a = 0. L ; :: thesis: eval ((Monom (a,b)),x) = a * (eval (b,x))

for b9 being bag of n holds (Monom (a,b)) . b9 = 0. L

proof

let b9 be bag of n; :: thesis: (Monom (a,b)) . b9 = 0. L

now :: thesis: ( ( b9 = b & (Monom (a,b)) . b9 = 0. L ) or ( b9 <> b & (Monom (a,b)) . b9 = 0. L ) )

per cases ( b9 = b or b9 <> b ) ;

case A3: b9 = b ; :: thesis: (Monom (a,b)) . b9 = 0. L

A4: b in Bags n by PRE_POLY:def 12;
A5: b in dom (b .--> a) by TARSKI:def 1;
dom (0_ (n,L)) = dom ((Bags n) --> (0. L)) by POLYNOM1:def 8
.= Bags n ;
then Monom (a,b) = (0_ (n,L)) +* (b .--> a) by A4, FUNCT_7:def 3;
hence (Monom (a,b)) . b9 = (b .--> a) . b by A3, A5, FUNCT_4:13
.= 0. L by A2, FUNCOP_1:72 ;
:: thesis: verum

end;

case b9 <> b ; :: thesis: (Monom (a,b)) . b9 = 0. L

hence (Monom (a,b)) . b9 = (0_ (n,L)) . b9 by FUNCT_7:32
.= 0. L by POLYNOM1:22 ;
:: thesis: verum

end;

end;

end;

hence (Monom (a,b)) . b9 = 0. L ; :: thesis: verum

end;

then A6: (Monom (a,b)) . (term (Monom (a,b))) = 0. L ;
thus eval ((Monom (a,b)),x) = (coefficient (Monom (a,b))) * (eval ((term (Monom (a,b))),x)) by Th12
.= 0. L by A6
.= a * (eval (b,x)) by A2 ; :: thesis: verum

end;

end;

end;

hence eval ((Monom (a,b)),x) = a * (eval (b,x)) ; :: thesis: verum