let n be Nat; :: thesis: for L being non empty ZeroStr
for p being Series of n,L holds (p extended_by_0) removed_last = p
let L be non empty ZeroStr ; :: thesis: for p being Series of n,L holds (p extended_by_0) removed_last = p
let p be Series of n,L; :: thesis: (p extended_by_0) removed_last = p
set e0 = p extended_by_0 ;
for a being Element of Bags n holds p . a = ((p extended_by_0) removed_last) . a

proof

let b be Element of Bags n; :: thesis: p . b = ((p extended_by_0) removed_last) . b
thus ((p extended_by_0) removed_last) . b = (p extended_by_0) . (b bag_extend 0) by Def6
.= p . b by HILB10_2:6 ; :: thesis: verum

end;

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