let n, m be Nat; :: thesis: for V, A being set
for loc being b₁ -valued Function
for d1 being NonatomicND of V,A
for pos being FinSequence
for prg being non empty FPrg (ND (b₁,b₂)) -valued FinSequence st 1 <= n & n <= len prg & (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m in dom (prg . n) holds
(prg . n) . ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m) is TypeSCNominativeData of V,A
let V, A be set ; :: thesis: for loc being V -valued Function
for d1 being NonatomicND of V,A
for pos being FinSequence
for prg being non empty FPrg (ND (V,A)) -valued FinSequence st 1 <= n & n <= len prg & (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m in dom (prg . n) holds
(prg . n) . ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m) is TypeSCNominativeData of V,A
let loc be V -valued Function; :: thesis: for d1 being NonatomicND of V,A
for pos being FinSequence
for prg being non empty FPrg (ND (V,A)) -valued FinSequence st 1 <= n & n <= len prg & (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m in dom (prg . n) holds
(prg . n) . ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m) is TypeSCNominativeData of V,A
let d1 be NonatomicND of V,A; :: thesis: for pos being FinSequence
for prg being non empty FPrg (ND (V,A)) -valued FinSequence st 1 <= n & n <= len prg & (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m in dom (prg . n) holds
(prg . n) . ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m) is TypeSCNominativeData of V,A
let pos be FinSequence; :: thesis: for prg being non empty FPrg (ND (V,A)) -valued FinSequence st 1 <= n & n <= len prg & (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m in dom (prg . n) holds
(prg . n) . ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m) is TypeSCNominativeData of V,A
let prg be non empty FPrg (ND (V,A)) -valued FinSequence; :: thesis: ( 1 <= n & n <= len prg & (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m in dom (prg . n) implies (prg . n) . ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m) is TypeSCNominativeData of V,A )
set F = PrgLocalOverlapSeq (A,loc,d1,prg,pos);
set P = prg . n;
assume that
A1: 1 <= n and
A2: n <= len prg and
A3: (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m in dom (prg . n) ; :: thesis: (prg . n) . ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m) is TypeSCNominativeData of V,A
n in dom prg by A1, A2, FINSEQ_3:25;
then prg . n in rng prg by FUNCT_1:def 3;
then A4: rng (prg . n) c= ND (V,A) by RELAT_1:def 19;
(prg . n) . ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m) in rng (prg . n) by A3, FUNCT_1:def 3;
hence (prg . n) . ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m) is TypeSCNominativeData of V,A by A4, NOMIN_1:39; :: thesis: verum