let S be COM-Struct ; :: thesis: for F, G being Program of S holds dom F c= dom (F ';' G)
let F, G be Program of S; :: thesis: dom F c= dom (F ';' G)
set P = F ';' G;
A1: dom (F ';' G) = (dom (CutLastLoc F)) \/ (dom (Reloc (G,((card F) -' 1)))) by FUNCT_4:def 1;
A2: dom F = (dom (CutLastLoc F)) \/ {(LastLoc F)} by VALUED_1:37;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom F or x in dom (F ';' G) )
assume A3: x in dom F ; :: thesis: x in dom (F ';' G)

per cases ( x in dom (CutLastLoc F) or x in {(LastLoc F)} ) by A2, A3, XBOOLE_0:def 3;

suppose x in dom (CutLastLoc F) ; :: thesis: x in dom (F ';' G)

hence x in dom (F ';' G) by A1, XBOOLE_0:def 3; :: thesis: verum

end;

suppose A4: x in {(LastLoc F)} ; :: thesis: x in dom (F ';' G)

then A5: x = LastLoc F by TARSKI:def 1;
reconsider f = x as Element of NAT by A4;
A6: f = (card F) -' 1 by A5, AFINSQ_1:70
.= ((card F) - 1) + 0 by PRE_CIRC:20 ;
card (F ';' G) = ((card F) + (card G)) - 1 by Th11
.= ((card F) - 1) + (card G) ;
then f < card (F ';' G) by A6, XREAL_1:6;
hence x in dom (F ';' G) by AFINSQ_1:66; :: thesis: verum

end;

end;