let n be Element of NAT ; :: thesis: for I, J being FinPartState of SCM+FSA holds ProgramPart (Relocated (I +* J),n) = (ProgramPart (Relocated I,n)) +* (ProgramPart (Relocated J,n))
let I, J be FinPartState of SCM+FSA ; :: thesis: ProgramPart (Relocated (I +* J),n) = (ProgramPart (Relocated I,n)) +* (ProgramPart (Relocated J,n))
A1: ( ProgramPart (Relocated I,n) = Reloc (ProgramPart I),n & ProgramPart (Relocated J,n) = Reloc (ProgramPart J),n ) by AMISTD_2:69;
thus ProgramPart (Relocated (I +* J),n) = Reloc (ProgramPart (I +* J)),n by AMISTD_2:69
.= IncAddr (Shift ((ProgramPart I) +* (ProgramPart J)),n),n by FUNCT_4:75
.= IncAddr ((Shift (ProgramPart I),n) +* (Shift (ProgramPart J),n)),n by VALUED_1:24
.= (ProgramPart (Relocated I,n)) +* (ProgramPart (Relocated J,n)) by A1, SCMFSA_4:25 ; :: thesis: verum