let I, J be Program of SCMPDS; :: thesis: dom (stop I) c= dom (stop (I ';' J))
set sI = stop I;
set sIJ = stop (I ';' J);
A1: card (stop (I ';' J)) = (card (I ';' J)) + 1 by Lm1, AFINSQ_1:17
.= ((card I) + (card J)) + 1 by AFINSQ_1:17
.= ((card I) + 1) + (card J) ;
card (stop I) = (card I) + 1 by Lm1, AFINSQ_1:17;
then A2: card (stop I) <= card (stop (I ';' J)) by A1, NAT_1:11;

now

set A = NAT ;
let x be set ; :: thesis: ( x in dom (stop I) implies x in dom (stop (I ';' J)) )
assume A3: x in dom (stop I) ; :: thesis: x in dom (stop (I ';' J))
dom (stop I) c= NAT by RELAT_1:def 18;
then reconsider l = x as Element of NAT by A3;
reconsider n = l as Element of NAT ;
n < card (stop I) by A3, AFINSQ_1:66;
then n < card (stop (I ';' J)) by A2, XXREAL_0:2;
hence x in dom (stop (I ';' J)) by AFINSQ_1:66; :: thesis: verum

end;

hence dom (stop I) c= dom (stop (I ';' J)) by TARSKI:def 3; :: thesis: verum