let s be SCM+FSA-State; :: thesis: for s9 being SCM-State holds s +* s9 is SCM+FSA-State
let s9 be SCM-State; :: thesis: s +* s9 is SCM+FSA-State
A1: dom SCM+FSA-OK = SCM+FSA-Memory by FUNCT_2:def 1;
reconsider f = SCM+FSA-OK as non-empty ManySortedSet of SCM+FSA-Memory ;
A2: dom s9 = dom SCM-OK by CARD_3:9
.= 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 by A2;

per cases ( x in {NAT} or x in SCM-Data-Loc ) 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:12
.= NAT by A7, AMI_2:6 ;
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:12;
SCM+FSA-OK . x = INT by A8, Th10;
hence s9 . x in f . x by A8, A10, A9, AMI_2:8; :: thesis: verum

end;

end;

end;

then s +* s9 is SCM+FSA-State by A1, A2, PRE_CIRC:6, XBOOLE_1:7;
hence s +* s9 is SCM+FSA-State ; :: thesis: verum