let I, J be Program of ; :: 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;
set A = NAT ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (stop I) or 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 Nat by A3;
reconsider n = l as 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