let R be non empty ZeroStr ; :: thesis: for p being AlgSequence of R holds
( p = <%(0. R)%> iff rng p = {(0. R)} )

let p be AlgSequence of R; :: thesis: ( p = <%(0. R)%> iff rng p = {(0. R)} )
thus ( p = <%(0. R)%> implies rng p = {(0. R)} ) :: thesis: ( rng p = {(0. R)} implies p = <%(0. R)%> )
proof
assume A1: p = <%(0. R)%> ; :: thesis: rng p = {(0. R)}
thus rng p c= {(0. R)} :: according to XBOOLE_0:def 10 :: thesis: {(0. R)} c= rng p
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng p or x in {(0. R)} )
assume x in rng p ; :: thesis: x in {(0. R)}
then consider i being object such that
A2: i in dom p and
A3: x = p . i by FUNCT_1:def 3;
reconsider i = i as Element of NAT by ;
p . i = 0. R by ;
hence x in {(0. R)} by ; :: thesis: verum
end;
thus {(0. R)} c= rng p :: thesis: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(0. R)} or x in rng p )
assume x in {(0. R)} ; :: thesis: x in rng p
then x = 0. R by TARSKI:def 1;
then A4: p . 0 = x by ;
dom p = NAT by FUNCT_2:def 1;
hence x in rng p by ; :: thesis: verum
end;
end;
thus ( rng p = {(0. R)} implies p = <%(0. R)%> ) :: thesis: verum
proof
assume A5: rng p = {(0. R)} ; :: thesis: p = <%(0. R)%>
A6: for k being Nat st k >= 0 holds
p . k = 0. R
proof
let k be Nat; :: thesis: ( k >= 0 implies p . k = 0. R )
k in NAT by ORDINAL1:def 12;
then k in dom p by FUNCT_2:def 1;
then p . k in rng p by FUNCT_1:def 3;
hence ( k >= 0 implies p . k = 0. R ) by ; :: thesis: verum
end;
for m being Nat st m is_at_least_length_of p holds
0 <= m by NAT_1:2;
then len p = 0 by ;
hence p = <%(0. R)%> by Th6; :: thesis: verum
end;