let L be non empty ZeroStr ; :: thesis: for z being Element of L holds rng <%z%> = {z,(0. L)}
let z be Element of L; :: thesis: rng <%z%> = {z,(0. L)}
set p = <%z%>;
A1: <%z%> . 0 = z by ALGSEQ_1:def 5;
A2: dom <%z%> = NAT by FUNCT_2:def 1;
thus rng <%z%> c= {z,(0. L)} :: according to XBOOLE_0:def 10 :: thesis: {z,(0. L)} c= rng <%z%>

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng <%z%> or y in {z,(0. L)} )
assume y in rng <%z%> ; :: thesis: y in {z,(0. L)}
then consider x being object such that
A3: x in dom <%z%> and
A4: <%z%> . x = y by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A3;

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

suppose x = 0 ; :: thesis: y in {z,(0. L)}

hence y in {z,(0. L)} by A4, A1, TARSKI:def 2; :: thesis: verum

end;

suppose x <> 0 ; :: thesis: y in {z,(0. L)}

then <%z%> . x = 0. L by POLYNOM5:32, NAT_1:14;
hence y in {z,(0. L)} by A4, TARSKI:def 2; :: thesis: verum

end;

end;

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in {z,(0. L)} or y in rng <%z%> )
assume y in {z,(0. L)} ; :: thesis: y in rng <%z%>

per cases then ( y = z or y = 0. L ) by TARSKI:def 2;

suppose y = z ; :: thesis: y in rng <%z%>

hence y in rng <%z%> by A1, A2, FUNCT_1:def 3; :: thesis: verum

end;

suppose A5: y = 0. L ; :: thesis: y in rng <%z%>

<%z%> . 1 = 0. L by POLYNOM5:32;
hence y in rng <%z%> by A2, A5, FUNCT_1:def 3; :: thesis: verum

end;

end;