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 CARD_1:def 7; :: 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:33;
hence f = i |-> 0 by A1, A3, FUNCOP_1:9, RELAT_1:42; :: thesis: verum

end;

end;