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 COMPOS_1:116;
thus ProgramPart (Relocated ((I +* J),n)) = Reloc ((ProgramPart (I +* J)),n) by COMPOS_1:116
.= 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