let S be State of SCM; :: thesis: for s being State of SCM+FSA st S = s | SCM-Memory holds
IC s = IC S
let s be State of SCM+FSA; :: thesis: ( S = s | SCM-Memory implies IC s = IC S )
assume S = s | SCM-Memory ; :: thesis: IC s = IC S
then s = s +* S by Th45;
hence IC s = IC S by Th46; :: thesis: verum