let n be Nat; :: thesis: for L being non empty ZeroStr
for p being Series of n,L holds {(0. L)} \/ (rng p) = rng (p extended_by_0)
let L be non empty ZeroStr ; :: thesis: for p being Series of n,L holds {(0. L)} \/ (rng p) = rng (p extended_by_0)
let p be Series of n,L; :: thesis: {(0. L)} \/ (rng p) = rng (p extended_by_0)
A1: ( dom p = Bags n & dom (p extended_by_0) = Bags (n + 1) ) by FUNCT_2:def 1;
A2: rng p c= rng (p extended_by_0)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng p or y in rng (p extended_by_0) )
assume y in rng p ; :: thesis: y in rng (p extended_by_0)
then consider x being object such that
A3: ( x in dom p & p . x = y ) by FUNCT_1:def 3;
reconsider x = x as Element of Bags n by A3;
(p extended_by_0) . (x bag_extend 0) = p . x by Th6;
hence y in rng (p extended_by_0) by A1, FUNCT_1:def 3, A3; :: thesis: verum

end;

set b0 = the bag of n bag_extend 1;
( the bag of n bag_extend 1) . n = 1 by HILBASIS:def 1;
then A4: (p extended_by_0) . ( the bag of n bag_extend 1) = 0. L by Def3;
0. L in rng (p extended_by_0) by A1, A4, FUNCT_1:def 3;
hence {(0. L)} \/ (rng p) c= rng (p extended_by_0) by A2, ZFMISC_1:137; :: according to XBOOLE_0:def 10 :: thesis: rng (p extended_by_0) c= {(0. L)} \/ (rng p)
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (p extended_by_0) or y in {(0. L)} \/ (rng p) )
assume y in rng (p extended_by_0) ; :: thesis: y in {(0. L)} \/ (rng p)
then consider x being object such that
A5: ( x in dom (p extended_by_0) & (p extended_by_0) . x = y ) by FUNCT_1:def 3;
reconsider x = x as Element of Bags (n + 1) by A5;

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

suppose x . n <> 0 ; :: thesis: y in {(0. L)} \/ (rng p)

then y = 0. L by A5, Def3;
hence y in {(0. L)} \/ (rng p) by ZFMISC_1:136; :: thesis: verum

end;

suppose x . n = 0 ; :: thesis: y in {(0. L)} \/ (rng p)

then A6: y = p . ((0,n) -cut x) by Def3, A5;
n -' 0 = n by NAT_D:40;
then (0,n) -cut x in Bags n by PRE_POLY:def 12;
then p . ((0,n) -cut x) in rng p by A1, FUNCT_1:def 3;
hence y in {(0. L)} \/ (rng p) by A6, ZFMISC_1:136; :: thesis: verum

end;

end;