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

( 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

thus
( rng p = {(0. R)} implies p = <%(0. R)%> )
:: thesis: verum
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

end;thus rng p c= {(0. R)} :: according to XBOOLE_0:def 10 :: thesis: {(0. R)} c= rng p

proof

thus
{(0. R)} c= rng p
:: thesis: verum
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;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

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

proof

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

A6: for k being Nat st k >= 0 holds

p . k = 0. R

0 <= m by NAT_1:2;

then len p = 0 by A6, Def2, Def3;

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

end;A6: for k being Nat st k >= 0 holds

p . k = 0. R

proof

for m being Nat st m is_at_least_length_of p holds
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;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

0 <= m by NAT_1:2;

then len p = 0 by A6, Def2, Def3;

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