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 ) ;
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;