set F = LocalOverlapSeq (A,loc,val,d1,size);

per cases ( n in dom (LocalOverlapSeq (A,loc,val,d1,size)) or not n in dom (LocalOverlapSeq (A,loc,val,d1,size)) ) ;

suppose n in dom (LocalOverlapSeq (A,loc,val,d1,size)) ; :: thesis: ( (LocalOverlapSeq (A,loc,val,d1,size)) . n is Function-like & (LocalOverlapSeq (A,loc,val,d1,size)) . n is Relation-like )

then ( 1 <= n & n <= len (LocalOverlapSeq (A,loc,val,d1,size)) ) by FINSEQ_3:25;
hence ( (LocalOverlapSeq (A,loc,val,d1,size)) . n is Function-like & (LocalOverlapSeq (A,loc,val,d1,size)) . n is Relation-like ) by Def6; :: thesis: verum

end;

suppose not n in dom (LocalOverlapSeq (A,loc,val,d1,size)) ; :: thesis: ( (LocalOverlapSeq (A,loc,val,d1,size)) . n is Function-like & (LocalOverlapSeq (A,loc,val,d1,size)) . n is Relation-like )

hence ( (LocalOverlapSeq (A,loc,val,d1,size)) . n is Function-like & (LocalOverlapSeq (A,loc,val,d1,size)) . n is Relation-like ) by FUNCT_1:def 2; :: thesis: verum

end;

end;