let N be set ; :: thesis: for n being Element of NAT
for S being AMI-Struct of N
for I, J being FinPartState of holds Shift (ProgramPart (I +* J)),n = (Shift (ProgramPart I),n) +* (Shift (ProgramPart J),n)
let n be Element of NAT ; :: thesis: for S being AMI-Struct of N
for I, J being FinPartState of holds Shift (ProgramPart (I +* J)),n = (Shift (ProgramPart I),n) +* (Shift (ProgramPart J),n)
let S be AMI-Struct of N; :: thesis: for I, J being FinPartState of holds Shift (ProgramPart (I +* J)),n = (Shift (ProgramPart I),n) +* (Shift (ProgramPart J),n)
let I, J be FinPartState of ; :: thesis: Shift (ProgramPart (I +* J)),n = (Shift (ProgramPart I),n) +* (Shift (ProgramPart J),n)
thus Shift (ProgramPart (I +* J)),n = Shift ((ProgramPart I) +* (ProgramPart J)),n by FUNCT_4:75
.= (Shift (ProgramPart I),n) +* (Shift (ProgramPart J),n) by VALUED_1:24 ; :: thesis: verum