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);

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)) ) )end;

hence
eval ((Monom (a,b)),x) = a * (eval (b,x))
; :: thesis: verumper cases
( a <> 0. L or a = 0. L )
;

end;

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;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

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

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;proof

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

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

hence
(Monom (a,b)) . b9 = 0. L
; :: thesis: verumper cases
( b9 = b or b9 <> b )
;

end;

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;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

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