let n be Nat; :: thesis: for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of (n + 1),L
for x being Function of n,L
for y being Function of (n + 1),L st not n in vars p & y | n = x holds
eval ((p removed_last),x) = eval (p,y)
let L be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for p being Polynomial of (n + 1),L
for x being Function of n,L
for y being Function of (n + 1),L st not n in vars p & y | n = x holds
eval ((p removed_last),x) = eval (p,y)
let p be Polynomial of (n + 1),L; :: thesis: for x being Function of n,L
for y being Function of (n + 1),L st not n in vars p & y | n = x holds
eval ((p removed_last),x) = eval (p,y)
let x be Function of n,L; :: thesis: for y being Function of (n + 1),L st not n in vars p & y | n = x holds
eval ((p removed_last),x) = eval (p,y)
let y be Function of (n + 1),L; :: thesis: ( not n in vars p & y | n = x implies eval ((p removed_last),x) = eval (p,y) )
assume A1: ( not n in vars p & y | n = x ) ; :: thesis: eval ((p removed_last),x) = eval (p,y)
thus eval ((p removed_last),x) = eval (((p removed_last) extended_by_0),y) by A1, HILB10_2:18
.= eval (p,y) by A1, Th50 ; :: thesis: verum