let L be non empty ZeroStr ; :: thesis: for z0 being Element of L holds
( <%z0%> . 0 = z0 & ( for n being Element of NAT st n >= 1 holds
<%z0%> . n = 0. L ) )
let z0 be Element of L; :: thesis: ( <%z0%> . 0 = z0 & ( for n being Element of NAT st n >= 1 holds
<%z0%> . n = 0. L ) )
thus <%z0%> . 0 = z0 by ALGSEQ_1:def 5; :: thesis: for n being Element of NAT st n >= 1 holds
<%z0%> . n = 0. L
let n be Element of NAT ; :: thesis: ( n >= 1 implies <%z0%> . n = 0. L )
A1: len <%z0%> <= 1 by ALGSEQ_1:def 5;
assume n >= 1 ; :: thesis: <%z0%> . n = 0. L
hence <%z0%> . n = 0. L by A1, ALGSEQ_1:8, XXREAL_0:2; :: thesis: verum