let i be Nat; :: thesis: for f being FinSequence of {0 } holds
( f = i |-> 0 iff len f = i )
let f be FinSequence of {0 }; :: thesis: ( f = i |-> 0 iff len f = i )
thus ( f = i |-> 0 implies len f = i ) by FINSEQ_1:def 18; :: thesis: ( len f = i implies f = i |-> 0 )
assume len f = i ; :: thesis: f = i |-> 0
then A1: dom f = Seg i by FINSEQ_1:def 3;

per cases ( Seg i = {} or Seg i <> {} ) ;

suppose A2: Seg i = {} ; :: thesis: f = i |-> 0

hence f = {} by A1
.= 0 |-> 0
.= i |-> 0 by A2 ;
:: thesis: verum

end;

suppose A3: Seg i <> {} ; :: thesis: f = i |-> 0

rng f c= {0 } by FINSEQ_1:def 4;
then ( rng f = {0 } or rng f = {} ) by ZFMISC_1:39;
hence f = i |-> 0 by A1, A3, FUNCOP_1:15, RELAT_1:65; :: thesis: verum

end;

end;