let s be SCM+FSA-State; :: thesis: for I being Element of SCM-Instr holds (s | SCM-Memory ) +* (NAT --> I) is SCM-State
let I be Element of SCM-Instr ; :: thesis: (s | SCM-Memory ) +* (NAT --> I) 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:90
.= SCM+FSA-Memory /\ SCM-Memory by A1, CARD_3:18
.= SCM-Memory by XBOOLE_1:21 ;

A3: now

let x be set ; :: thesis: ( x in dom SCM-OK implies ((s | SCM-Memory ) +* (NAT --> I)) . b₁ in SCM-OK . b₁ )
A4: NAT = dom (NAT --> I) by FUNCOP_1:19;
assume x in dom SCM-OK ; :: thesis: ((s | SCM-Memory ) +* (NAT --> I)) . b₁ in SCM-OK . b₁
then A5: x in SCM-Memory by FUNCT_2:def 1;
then A6: ( x in {NAT } \/ SCM-Data-Loc or x in NAT ) by XBOOLE_0:def 3;

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

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

then not x in NAT by TARSKI:def 1;
then A8: ((s | SCM-Memory ) +* (NAT --> I)) . x = (s | SCM-Memory ) . x by A4, FUNCT_4:12
.= s . x by A2, A5, FUNCT_1:70 ;
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:22;
hence ((s | SCM-Memory ) +* (NAT --> I)) . x in SCM-OK . x by A10, A8, A9, AMI_2:7, AMI_2:30; :: thesis: verum

end;

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

then SCM-OK . x = INT by AMI_2:10;
then not x in NAT by AMI_2:6, AMI_2:11;
then A12: ((s | SCM-Memory ) +* (NAT --> I)) . x = (s | SCM-Memory ) . x by A4, FUNCT_4:12
.= s . x by A2, A5, FUNCT_1:70 ;
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:22
.= INT by A11, Th10 ;
s . a in pi (product SCM+FSA-OK ),a by CARD_3:def 6;
hence ((s | SCM-Memory ) +* (NAT --> I)) . x in SCM-OK . x by A11, A12, A13, AMI_2:10; :: thesis: verum

end;

suppose A14: x in NAT ; :: thesis: ((s | SCM-Memory ) +* (NAT --> I)) . b₁ in SCM-OK . b₁

then A15: SCM-OK . x = SCM-Instr by AMI_2:11;
((s | SCM-Memory ) +* (NAT --> I)) . x = (NAT --> I) . x by A4, A14, FUNCT_4:14
.= I by A14, FUNCOP_1:13 ;
hence ((s | SCM-Memory ) +* (NAT --> I)) . x in SCM-OK . x by A15; :: thesis: verum

end;

end;

end;

dom ((s | SCM-Memory ) +* (NAT --> I)) = (dom (s | SCM-Memory )) \/ (dom (NAT --> I)) by FUNCT_4:def 1
.= SCM-Memory \/ NAT by A2, FUNCOP_1:19
.= SCM-Memory by XBOOLE_1:12
.= dom SCM-OK by FUNCT_2:def 1 ;
hence (s | SCM-Memory ) +* (NAT --> I) is SCM-State by A3, CARD_3:18; :: thesis: verum