per cases ( n in dom <*0*> or not n in dom <*0*> ) ;

suppose n in dom <*0*> ; :: thesis: <*0*> . n = 0

then n in Seg 1 by FINSEQ_1:38;
then ( 1 <= n & n <= 1 ) by FINSEQ_1:1;
then n = 1 by XXREAL_0:1;
hence <*0*> . n = 0 ; :: thesis: verum

end;

suppose not n in dom <*0*> ; :: thesis: <*0*> . n = 0

hence <*0*> . n = 0 by FUNCT_1:def 2; :: thesis: verum

end;

end;