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 set ; :: 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 set such that
A2: ( i in dom p & x = p . i ) by FUNCT_1:def 5;
reconsider i = i as Element of NAT by A2, FUNCT_2:def 1;
p . i = 0. R by A1, Th33;
hence x in {(0. R)} by A2, TARSKI:def 1; :: thesis: verum

end;

thus {(0. R)} c= rng p :: thesis: verum

proof

let x be set ; :: 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 A3: p . 0 = x by A1, Def6;
dom p = NAT by FUNCT_2:def 1;
hence x in rng p by A3, FUNCT_1:def 5; :: thesis: verum

end;

end;

thus ( rng p = {(0. R)} implies p = <%(0. R)%> ) :: thesis: verum

proof

assume A4: rng p = {(0. R)} ; :: thesis: p = <%(0. R)%>
len p = 0

proof

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 13;
then k in dom p by FUNCT_2:def 1;
then p . k in rng p by FUNCT_1:def 5;
hence ( k >= 0 implies p . k = 0. R ) by A4, TARSKI:def 1; :: thesis: verum

end;

then A5: 0 is_at_least_length_of p by Def3;
for m being Nat st m is_at_least_length_of p holds
0 <= m by NAT_1:2;
hence len p = 0 by A5, Def4; :: thesis: verum

end;

hence p = <%(0. R)%> by Th31; :: thesis: verum

end;