let n be Nat; :: thesis: for L being non empty ZeroStr
for p being Series of (n + 1),L st not n in vars p holds
(p removed_last) extended_by_0 = p
let L be non empty ZeroStr ; :: thesis: for p being Series of (n + 1),L st not n in vars p holds
(p removed_last) extended_by_0 = p
let p be Series of (n + 1),L; :: thesis: ( not n in vars p implies (p removed_last) extended_by_0 = p )
assume A1: not n in vars p ; :: thesis: (p removed_last) extended_by_0 = p
set r = p removed_last ;
for a being Element of Bags (n + 1) holds p . a = ((p removed_last) extended_by_0) . a

proof

let b be Element of Bags (n + 1); :: thesis: p . b = ((p removed_last) extended_by_0) . b

per cases ( b . n <> 0 or b . n = 0 ) ;

suppose A2: b . n <> 0 ; :: thesis: p . b = ((p removed_last) extended_by_0) . b

then A3: ((p removed_last) extended_by_0) . b = 0. L by HILB10_2:def 3;
A4: Bags (n + 1) = dom p by PARTFUN1:def 2;
not b in Support p by A1, A2, Def5;
hence p . b = ((p removed_last) extended_by_0) . b by A3, A4, POLYNOM1:def 3; :: thesis: verum

end;

suppose A5: b . n = 0 ; :: thesis: p . b = ((p removed_last) extended_by_0) . b

then A6: ((p removed_last) extended_by_0) . b = (p removed_last) . ((0,n) -cut b) by HILB10_2:def 3;
set c = (0,n) -cut b;
n -' 0 = n - 0 ;
then (p removed_last) . ((0,n) -cut b) = p . (((0,n) -cut b) bag_extend 0) by Def6;
hence p . b = ((p removed_last) extended_by_0) . b by A6, A5, HILB10_2:4; :: thesis: verum

end;

end;

end;

hence (p removed_last) extended_by_0 = p ; :: thesis: verum