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
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
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
for x being Function of n,L holds eval (Monom a,b),x = a * (eval b,x)
let b be bag of ; :: 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

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 by STRUCT_0:def 15;
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 b' being bag of holds (Monom a,b) . b' = 0. L

proof

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

now

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

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

A4: dom (0_ n,L) = dom ((Bags n) --> (0. L)) by POLYNOM1:def 24
.= Bags n by FUNCOP_1:19 ;
b in Bags n by POLYNOM1:def 14;
then A5: Monom a,b = (0_ n,L) +* (b .--> a) by A4, FUNCT_7:def 3;
dom (b .--> a) = {b} by FUNCOP_1:19;
then b in dom (b .--> a) by TARSKI:def 1;
hence (Monom a,b) . b' = (b .--> a) . b by A3, A5, FUNCT_4:14
.= 0. L by A2, FUNCOP_1:87 ;
:: thesis: verum

end;

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

hence (Monom a,b) . b' = (0_ n,L) . b' by FUNCT_7:34
.= 0. L by POLYNOM1:81 ;
:: thesis: verum

end;

end;

end;

hence (Monom a,b) . b' = 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, VECTSP_1:39
.= a * (eval b,x) by A2, VECTSP_1:39 ; :: thesis: verum

end;

end;

end;

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