let s be SCM+FSA-State; :: thesis: for I being Element of SCM-Instr holds s | SCM-Memory is SCM-State
let I be Element of SCM-Instr ; :: thesis: s | SCM-Memory is SCM-State
A1: dom (s | SCM-Memory) = (dom s) /\ SCM-Memory by RELAT_1:61
.= SCM+FSA-Memory /\ SCM-Memory by Lm8, CARD_3:9
.= SCM-Memory by XBOOLE_1:21 ;

A2: now :: thesis: for x being object st x in dom (SCM-VAL * SCM-OK) holds
(s | SCM-Memory) . x in (SCM-VAL * SCM-OK) . x

let x be object ; :: thesis: ( x in dom (SCM-VAL * SCM-OK) implies (s | SCM-Memory) . b₁ in (SCM-VAL * SCM-OK) . b₁ )
assume x in dom (SCM-VAL * SCM-OK) ; :: thesis: (s | SCM-Memory) . b₁ in (SCM-VAL * SCM-OK) . b₁
then A3: x in SCM-Memory by AMI_2:27;
then A4: x in {NAT} \/ SCM-Data-Loc ;

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

suppose A5: x in {NAT} ; :: thesis: (s | SCM-Memory) . b₁ in (SCM-VAL * SCM-OK) . b₁

A6: (s | SCM-Memory) . x = (s | SCM-Memory) . x
.= s . x by A1, A3, FUNCT_1:47 ;
reconsider a = x as Element of SCM+FSA-Memory by A3, Th1;
A7: s . a in pi ((product (SCM*-VAL * SCM+FSA-OK)),a) by CARD_3:def 6;
A8: x = NAT by A5, TARSKI:def 1;
dom (SCM*-VAL * SCM+FSA-OK) = SCM+FSA-Memory by Lm8;
then pi ((product (SCM*-VAL * SCM+FSA-OK)),a) = NAT by A8, Th4, CARD_3:12;
hence (s | SCM-Memory) . x in (SCM-VAL * SCM-OK) . x by A8, A6, A7, AMI_2:6; :: thesis: verum

end;

suppose A9: x in SCM-Data-Loc ; :: thesis: (s | SCM-Memory) . b₁ in (SCM-VAL * SCM-OK) . b₁

A10: (s | SCM-Memory) . x = (s | SCM-Memory) . x
.= s . x by A1, A3, FUNCT_1:47 ;
reconsider a = x as Element of SCM+FSA-Memory by A3, Th1;
dom (SCM*-VAL * SCM+FSA-OK) = SCM+FSA-Memory by Lm8;
then A11: pi ((product (SCM*-VAL * SCM+FSA-OK)),a) = (SCM*-VAL * SCM+FSA-OK) . a by CARD_3:12
.= INT by A9, Th5 ;
s . a in pi ((product (SCM*-VAL * SCM+FSA-OK)),a) by CARD_3:def 6;
hence (s | SCM-Memory) . x in (SCM-VAL * SCM-OK) . x by A9, A10, A11, AMI_2:8; :: thesis: verum

end;

end;

end;

dom (s | SCM-Memory) = dom (s | SCM-Memory)
.= SCM-Memory by A1
.= dom (SCM-VAL * SCM-OK) by AMI_2:27 ;
hence s | SCM-Memory is SCM-State by A2, CARD_3:9; :: thesis: verum