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;