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 ;

hence s +* s1 is SCM+FSA-State ; :: thesis: verum

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

then
s +* s1 is SCM+FSA-State
by A1, A2, PRE_CIRC:6, XBOOLE_1:7;s1 . x in f . x

let x be set ; :: thesis: ( x in dom s1 implies s1 . b_{1} in f . b_{1} )

assume A3: x in dom s1 ; :: thesis: s1 . b_{1} in f . b_{1}

then A4: x in {NAT} \/ SCM-Data-Loc by A2;

end;assume A3: x in dom s1 ; :: thesis: s1 . 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;

end;

suppose A5:
x in {NAT}
; :: thesis: s1 . b_{1} in f . b_{1}

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;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

suppose A8:
x in SCM-Data-Loc
; :: thesis: s1 . b_{1} in f . b_{1}

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;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

hence s +* s1 is SCM+FSA-State ; :: thesis: verum