let I, J be Program of SCMPDS ; :: thesis: Initialize I c= Initialize (stop (I ';' J))
set SA0 = Start-At 0 ,SCMPDS ;
set IS = I ';' (J ';' (Stop SCMPDS ));
set Ip = Initialize (stop (I ';' J));
A1: Initialize (stop (I ';' J)) = (I ';' (J ';' (Stop SCMPDS ))) +* (Start-At 0 ,SCMPDS ) by SCMPDS_4:46;
A2: I c= I ';' (J ';' (Stop SCMPDS )) by SCMPDS_4:40;
dom (I ';' (J ';' (Stop SCMPDS ))) misses dom (Start-At 0 ,SCMPDS ) by SCMPDS_4:54;
then I ';' (J ';' (Stop SCMPDS )) c= Initialize (stop (I ';' J)) by A1, FUNCT_4:33;
then A3: I c= Initialize (stop (I ';' J)) by A2, XBOOLE_1:1;
dom I misses dom (Start-At 0 ,SCMPDS ) by SCMPDS_4:54;
then A4: I \/ (Start-At 0 ,SCMPDS ) = Initialize I by FUNCT_4:32;
Start-At 0 ,SCMPDS c= Initialize (stop (I ';' J)) by FUNCT_4:26;
hence Initialize I c= Initialize (stop (I ';' J)) by A3, A4, XBOOLE_1:8; :: thesis: verum