f . i in Segm 16

proof

per cases ( i in dom f or not i in dom f ) ;

suppose i in dom f ; :: thesis: f . i in Segm 16

hence f . i in Segm 16 by FUNCT_2:5; :: thesis: verum

end;

suppose not i in dom f ; :: thesis: f . i in Segm 16

then f . i = 0 by FUNCT_1:def 2;
hence f . i in Segm 16 by NAT_1:44; :: thesis: verum

end;

end;

end;

hence f . i is Element of 16 ; :: thesis: verum