let n be Nat; :: thesis: for L being non empty ZeroStr
for p being Series of n,L
for b being bag of n + 1 st b . n = 0 holds
( b in Support (p extended_by_0) iff (0,n) -cut b in Support p )
let L be non empty ZeroStr ; :: thesis: for p being Series of n,L
for b being bag of n + 1 st b . n = 0 holds
( b in Support (p extended_by_0) iff (0,n) -cut b in Support p )
let p be Series of n,L; :: thesis: for b being bag of n + 1 st b . n = 0 holds
( b in Support (p extended_by_0) iff (0,n) -cut b in Support p )
let b be bag of n + 1; :: thesis: ( b . n = 0 implies ( b in Support (p extended_by_0) iff (0,n) -cut b in Support p ) )
assume A1: b . n = 0 ; :: thesis: ( b in Support (p extended_by_0) iff (0,n) -cut b in Support p )
A2: n -' 0 = n by NAT_D:40;
b = ((0,n) -cut b) bag_extend 0 by A1, Th4;
hence ( b in Support (p extended_by_0) iff (0,n) -cut b in Support p ) by Th8, A2; :: thesis: verum