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) = IncAddr [(Shift (ProgramPart I),n)],n & ProgramPart (Relocated J,n) = IncAddr [(Shift (ProgramPart J),n)],n ) by SCMFSA_5:2;
thus ProgramPart (Relocated (I +* J),n) = IncAddr [(Shift (ProgramPart (I +* J)),n)],n by SCMFSA_5:2
.= 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