let p be PartState of SCM+FSA; :: thesis: Initialize (Initialized p) = Initialized p
thus Initialize (Initialized p) = (Initialized p) +* (Start-At (0,SCM+FSA))
.= p +* ((Initialize ((intloc 0) .--> 1)) +* (Start-At (0,SCM+FSA))) by FUNCT_4:15
.= Initialized p by FUNCT_4:99 ; :: thesis: verum