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

now

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

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

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

then A7: x = IC SCM by TARSKI:def 1;
then not x in NAT by AMI_3:4;
then A8: ((s | SCM-Memory ) +* (NAT --> I)) . x = (s | SCM-Memory ) . x by A6, FUNCT_4:12
.= s . x by A2, A4, FUNCT_1:70 ;
reconsider a = x as Element of SCM+FSA-Memory by A4, Th1;
dom SCM+FSA-OK = SCM+FSA-Memory by FUNCT_2:def 1;
then A9: pi (product SCM+FSA-OK ),a = NAT by A7, Th9, AMI_3:4, CARD_3:22;
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 A7, A8, A9, AMI_2:7, AMI_2:30, AMI_3:4; :: thesis: verum

end;

suppose A10: 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 A11: ((s | SCM-Memory ) +* (NAT --> I)) . x = (s | SCM-Memory ) . x by A6, FUNCT_4:12
.= s . x by A2, A4, FUNCT_1:70 ;
reconsider a = x as Element of SCM+FSA-Memory by A4, Th1;
dom SCM+FSA-OK = SCM+FSA-Memory by FUNCT_2:def 1;
then A12: pi (product SCM+FSA-OK ),a = SCM+FSA-OK . a by CARD_3:22
.= INT by A10, 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 A10, A11, A12, AMI_2:10; :: thesis: verum

end;

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

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

end;

end;

end;

hence (s | SCM-Memory ) +* (NAT --> I) is SCM-State by A3, CARD_3:18; :: thesis: verum