set F = PrgLocalOverlapSeq (A,loc,d1,prg,pos);

per cases ( n in dom (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) or not n in dom (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) ) ;

suppose n in dom (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) ; :: thesis: ( (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n is Function-like & (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n is Relation-like )

then ( 1 <= n & n <= len (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) ) by FINSEQ_3:25;
hence ( (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n is Function-like & (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n is Relation-like ) by NOMIN_7:def 6; :: thesis: verum

end;

suppose not n in dom (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) ; :: thesis: ( (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n is Function-like & (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n is Relation-like )

hence ( (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n is Function-like & (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n is Relation-like ) by FUNCT_1:def 2; :: thesis: verum

end;

end;