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

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