let s be SCM+FSA-State; :: thesis: for s1 being SCM-State holds s +* s1 is SCM+FSA-State
let s1 be SCM-State; :: thesis: s +* s1 is SCM+FSA-State
A1: dom (SCM*-VAL * SCM+FSA-OK) = SCM+FSA-Memory by Lm8;
then reconsider f = SCM*-VAL * SCM+FSA-OK as non-empty ManySortedSet of SCM+FSA-Memory by PARTFUN1:def 2;
A2: dom s1 = dom (SCM-VAL * SCM-OK) by CARD_3:9
.= SCM-Memory by AMI_2:27 ;

now :: thesis: for x being set st x in dom s1 holds
s1 . x in f . x

let x be set ; :: thesis: ( x in dom s1 implies s1 . b₁ in f . b₁ )
assume A3: x in dom s1 ; :: thesis: s1 . 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: s1 . b₁ in f . b₁

reconsider a = x as Element of SCM-Memory by A2, A3;
A6: s1 . a in pi ((product (SCM-VAL * SCM-OK)),a) by CARD_3:def 6;
A7: x = NAT by A5, TARSKI:def 1;
dom (SCM-VAL * SCM-OK) = SCM-Memory by AMI_2:27;
then pi ((product (SCM-VAL * SCM-OK)),a) = (SCM-VAL * SCM-OK) . a by CARD_3:12
.= NAT by A7, AMI_2:6 ;
hence s1 . x in f . x by A5, A6, Th4, TARSKI:def 1; :: thesis: verum

end;

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

reconsider a = x as Element of SCM-Memory by A2, A3;
A9: s1 . a in pi ((product (SCM-VAL * SCM-OK)),a) by CARD_3:def 6;
dom (SCM-VAL * SCM-OK) = SCM-Memory by AMI_2:27;
then A10: pi ((product (SCM-VAL * SCM-OK)),a) = (SCM-VAL * SCM-OK) . a by CARD_3:12;
(SCM*-VAL * SCM+FSA-OK) . x = INT by A8, Th5;
hence s1 . x in f . x by A8, A10, A9, AMI_2:8; :: thesis: verum

end;

end;

end;

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