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 A2, FUNCT_2:def 1;
p . i = 0. R by A1, Th7;
hence x in {(0. R)} by A3, TARSKI:def 1; :: 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 A1, Def4;
dom p = NAT by FUNCT_2:def 1;
hence x in rng p by A4, FUNCT_1:def 3; :: 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 A5, TARSKI:def 1; :: 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 A6, Def2, Def3;
hence p = <%(0. R)%> by Th6; :: thesis: verum

end;