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