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 SCM+FSA-OK = SCM+FSA-Memory by FUNCT_2:def 1;
A2: dom (s | SCM-Memory) = (dom s) /\ SCM-Memory by RELAT_1:61
.= SCM+FSA-Memory /\ SCM-Memory by A1, CARD_3:9
.= SCM-Memory by XBOOLE_1:21 ;

A3: now

let x be set ; :: thesis: ( x in dom SCM-OK implies (s | SCM-Memory) . b₁ in SCM-OK . b₁ )
assume x in dom SCM-OK ; :: thesis: (s | SCM-Memory) . b₁ in SCM-OK . b₁
then A5: x in SCM-Memory by FUNCT_2:def 1;
then A6: x in {NAT} \/ SCM-Data-Loc ;

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

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

A8: (s | SCM-Memory) . x = (s | SCM-Memory) . x
.= s . x by A2, A5, FUNCT_1:47 ;
reconsider a = x as Element of SCM+FSA-Memory by A5, Th1;
A9: s . a in pi ((product SCM+FSA-OK),a) by CARD_3:def 6;
A10: x = NAT by A7, TARSKI:def 1;
dom SCM+FSA-OK = SCM+FSA-Memory by FUNCT_2:def 1;
then pi ((product SCM+FSA-OK),a) = NAT by A10, Th9, CARD_3:12;
hence (s | SCM-Memory) . x in SCM-OK . x by A10, A8, A9, AMI_2:6, AMI_2:22; :: thesis: verum

end;

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

A12: (s | SCM-Memory) . x = (s | SCM-Memory) . x
.= s . x by A2, A5, FUNCT_1:47 ;
reconsider a = x as Element of SCM+FSA-Memory by A5, Th1;
dom SCM+FSA-OK = SCM+FSA-Memory by FUNCT_2:def 1;
then A13: pi ((product SCM+FSA-OK),a) = SCM+FSA-OK . a by CARD_3:12
.= INT by A11, Th10 ;
s . a in pi ((product SCM+FSA-OK),a) by CARD_3:def 6;
hence (s | SCM-Memory) . x in SCM-OK . x by A11, A12, A13, AMI_2:8; :: thesis: verum

end;

end;

end;

dom (s | SCM-Memory) = dom (s | SCM-Memory)
.= SCM-Memory by A2
.= SCM-Memory
.= dom SCM-OK by FUNCT_2:def 1 ;
hence s | SCM-Memory is SCM-State by A3, CARD_3:9; :: thesis: verum