let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N
for I, J being Program of S holds dom I misses dom (Reloc ((ProgramPart J),(card I)))
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N; :: thesis: for I, J being Program of S holds dom I misses dom (Reloc ((ProgramPart J),(card I)))
let I, J be Program of S; :: thesis: dom I misses dom (Reloc ((ProgramPart J),(card I)))
assume A1: dom I meets dom (Reloc ((ProgramPart J),(card I))) ; :: thesis: contradiction
dom (Reloc ((ProgramPart J),(card I))) = dom (Reloc (J,(card I))) by RELAT_1:209
.= dom (Shift (J,(card I))) by Def40
.= { (l + (card I)) where l is Element of NAT : l in dom J } by VALUED_1:def 12 ;
then consider x being set such that
A2: x in dom I and
A3: x in { (l + (card I)) where l is Element of NAT : l in dom J } by A1, XBOOLE_0:3;
consider l being Element of NAT such that
A4: x = l + (card I) and
l in dom J by A3;
l + (card I) < card I by A2, A4, AFINSQ_1:70;
hence contradiction by NAT_1:11; :: thesis: verum