let s be SCM+FSA-State; :: thesis: for s9 being SCM-State holds (s +* s9) +* (s | NAT) is SCM+FSA-State
let s9 be SCM-State; :: thesis: (s +* s9) +* (s | NAT) is SCM+FSA-State
A1: dom SCM+FSA-OK = SCM+FSA-Memory by FUNCT_2:def 1;
then reconsider f = SCM+FSA-OK as non-empty ManySortedSet of SCM+FSA-Memory by PARTFUN1:def 4;
A2: dom s9 = dom SCM-OK by CARD_3:18
.= SCM-Memory by FUNCT_2:def 1 ;

now

let x be set ; :: thesis: ( x in dom s9 implies s9 . b₁ in f . b₁ )
assume A3: x in dom s9 ; :: thesis: s9 . b₁ in f . b₁
then A4: ( x in {NAT} \/ SCM-Data-Loc or x in NAT ) by A2, XBOOLE_0:def 3;

per cases ( x in {NAT} or x in SCM-Data-Loc or x in NAT ) by A4, XBOOLE_0:def 3;

suppose A5: x in {NAT} ; :: thesis: s9 . b₁ in f . b₁

reconsider a = x as Element of SCM-Memory by A2, A3;
A6: s9 . a in pi ((product SCM-OK),a) by CARD_3:def 6;
A7: x = NAT by A5, TARSKI:def 1;
dom SCM-OK = SCM-Memory by FUNCT_2:def 1;
then pi ((product SCM-OK),a) = SCM-OK . a by CARD_3:22
.= NAT by A7, AMI_2:7 ;
hence s9 . x in f . x by A5, A6, Th9, TARSKI:def 1; :: thesis: verum

end;

suppose A8: x in SCM-Data-Loc ; :: thesis: s9 . b₁ in f . b₁

reconsider a = x as Element of SCM-Memory by A2, A3;
A9: s9 . a in pi ((product SCM-OK),a) by CARD_3:def 6;
dom SCM-OK = SCM-Memory by FUNCT_2:def 1;
then A10: pi ((product SCM-OK),a) = SCM-OK . a by CARD_3:22;
SCM+FSA-OK . x = INT by A8, Th10;
hence s9 . x in f . x by A8, A10, A9, AMI_2:10; :: thesis: verum

end;

suppose A11: x in NAT ; :: thesis: s9 . b₁ in f . b₁

SCM+FSA-Instr = (SCM-Instr \/ ( { [J,{},<*c,f2,b*>] where J is Element of Segm 14, c, b is Element of SCM+FSA-Data-Loc , f2 is Element of SCM+FSA-Data*-Loc : J in {9,10} } \/ { [K,{},<*c1,f1*>] where K is Element of Segm 14, c1 is Element of SCM+FSA-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } )) \/ { [13,{},<*b1*>] where b1 is Element of SCM+FSA-Data-Loc : verum } by XBOOLE_1:4
.= SCM-Instr \/ (( { [J,{},<*c,f2,b*>] where J is Element of Segm 14, c, b is Element of SCM+FSA-Data-Loc , f2 is Element of SCM+FSA-Data*-Loc : J in {9,10} } \/ { [K,{},<*c1,f1*>] where K is Element of Segm 14, c1 is Element of SCM+FSA-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } ) \/ { [13,{},<*b1*>] where b1 is Element of SCM+FSA-Data-Loc : verum } ) by XBOOLE_1:4 ;
then A12: SCM-Instr c= SCM+FSA-Instr by XBOOLE_1:7;
reconsider a = x as Element of SCM-Memory by A2, A3;
A13: s9 . a in pi ((product SCM-OK),a) by CARD_3:def 6;
dom SCM-OK = SCM-Memory by FUNCT_2:def 1;
then A14: pi ((product SCM-OK),a) = SCM-OK . a by CARD_3:22;
( SCM-OK . x = SCM-Instr & SCM+FSA-OK . x = SCM+FSA-Instr ) by A11, Th11, AMI_2:11;
hence s9 . x in f . x by A12, A14, A13; :: thesis: verum

end;

end;

end;

then s +* s9 is SCM+FSA-State by A1, A2, PRE_CIRC:9, XBOOLE_1:7;
hence (s +* s9) +* (s | NAT) is SCM+FSA-State by CARD_3:69; :: thesis: verum