let s be State of SCM+FSA; :: thesis: for I1, I2 being Program of SCM+FSA
for l being Element of NAT holds NPP (s +* (NPP (I1 +* (Start-At (l,SCM+FSA))))) = NPP (s +* (NPP (I2 +* (Start-At (l,SCM+FSA)))))
let I1, I2 be Program of SCM+FSA; :: thesis: for l being Element of NAT holds NPP (s +* (NPP (I1 +* (Start-At (l,SCM+FSA))))) = NPP (s +* (NPP (I2 +* (Start-At (l,SCM+FSA)))))
let l be Element of NAT ; :: thesis: NPP (s +* (NPP (I1 +* (Start-At (l,SCM+FSA))))) = NPP (s +* (NPP (I2 +* (Start-At (l,SCM+FSA)))))
A1: NPP (I1 +* (Start-At (l,SCM+FSA))) = NPP (Start-At (l,SCM+FSA)) by COMPOS_1:224
.= Start-At (l,SCM+FSA) by COMPOS_1:212 ;
NPP (I2 +* (Start-At (l,SCM+FSA))) = NPP (Start-At (l,SCM+FSA)) by COMPOS_1:224
.= Start-At (l,SCM+FSA) by COMPOS_1:212 ;
hence NPP (s +* (NPP (I1 +* (Start-At (l,SCM+FSA))))) = NPP (s +* (NPP (I2 +* (Start-At (l,SCM+FSA))))) by A1; :: thesis: verum