set S1 = {(IC )};
set S2 = SCM-Data-Loc ;
set S3 = NAT ;
defpred S₁[ set , set ] means ex m being Element of NAT st
( ( $1 = IC & $2 = F₃() ) or ( $1 = m & $2 = F₁(m) ) or ( $1 = DataLoc (m,0) & $2 = F₂(m) ) );
A1: for e being set st e in the carrier of SCMPDS holds
ex u being set st S₁[e,u]

proof

let e be set ; :: thesis:
assume e in the carrier of SCMPDS ; :: thesis:
then e in ({(IC )} \/ SCM-Data-Loc) \/ NAT by COMPOS_1:160, SCMPDS_2:100;
then A2: ( e in {(IC )} \/ SCM-Data-Loc or e in NAT ) by XBOOLE_0:def 3;

now

per cases by A2, XBOOLE_0:def 3;

case e in {(IC )} ; :: thesis:

hence e = IC by TARSKI:def 1; :: thesis:

end;

case e in SCM-Data-Loc ; :: thesis:

then e is Int_position by SCMPDS_2:9;
hence ex m being Element of NAT st e = DataLoc (m,0) by Th18; :: thesis:

end;

case e in NAT ; :: thesis:

then reconsider l = e as Element of NAT ;
reconsider m = l as Element of NAT ;
e = m ;
hence ex m being Element of NAT st e = m ; :: thesis:

end;

end;

end;

then consider m being Element of NAT such that
A3: ( e = IC or e = m or e = DataLoc (m,0) ) ;

per cases by A3;

suppose A4: e = IC ; :: thesis:

take u = F₃(); :: thesis:
thus S₁[e,u] by A4; :: thesis:

end;

suppose A5: e = m ; :: thesis:

take u = F₁(m); :: thesis:
thus S₁[e,u] by A5; :: thesis:

end;

suppose A6: e = DataLoc (m,0) ; :: thesis:

take u = F₂(m); :: thesis:
thus S₁[e,u] by A6; :: thesis:

end;

end;

end;

consider f being Function such that
A7: dom f = the carrier of SCMPDS and
A8: for e being set st e in the carrier of SCMPDS holds
S₁[e,f . e] from CLASSES1:sch 1(A1);
A9: dom the Object-Kind of SCMPDS = the carrier of SCMPDS by FUNCT_2:def 1;

now

let x be set ; :: thesis:
assume A10: x in dom the Object-Kind of SCMPDS ; :: thesis:
then x in ({(IC )} \/ SCM-Data-Loc) \/ NAT by A9, COMPOS_1:160, SCMPDS_2:100;
then A11: ( x in {(IC )} \/ SCM-Data-Loc or x in NAT ) by XBOOLE_0:def 3;
consider m being Element of NAT such that
A12: ( ( x = IC & f . x = F₃() ) or ( x = m & f . x = F₁(m) ) or ( x = DataLoc (m,0) & f . x = F₂(m) ) ) by A8, A9, A10;

per cases by A11, XBOOLE_0:def 3;

suppose x in SCM-Data-Loc ; :: thesis:

then A13: x is Int_position by SCMPDS_2:9;
then the Object-Kind of SCMPDS . x = ObjectKind (DataLoc (m,0)) by A12, SCMPDS_2:52, SCMPDS_2:53
.= INT by SCMPDS_2:13 ;
hence f . x in the Object-Kind of SCMPDS . x by A12, A13, INT_1:def 2, SCMPDS_2:53; :: thesis:

end;

suppose A14: x in {(IC )} ; :: thesis:

then the Object-Kind of SCMPDS . x = ObjectKind (IC ) by TARSKI:def 1
.= NAT by COMPOS_1:def 6 ;
hence f . x in the Object-Kind of SCMPDS . x by A12, A14, SCMPDS_2:6, TARSKI:def 1; :: thesis:

end;

suppose x in NAT ; :: thesis:

then reconsider l = x as Element of NAT ;
the Object-Kind of SCMPDS . l = the Instructions of SCMPDS by COMPOS_1:def 8;
hence f . x in the Object-Kind of SCMPDS . x by A12, COMPOS_1:3, SCMPDS_2:53; :: thesis:

end;

end;

end;

then reconsider f = f as State of SCMPDS by A7, A9, FUNCT_1:def 20, PARTFUN1:def 4, RELAT_1:def 18;
consider m being Element of NAT such that
A15: ( ( IC = IC & f . (IC ) = F₃() ) or ( IC = m & f . (IC ) = F₁(m) ) or ( IC = DataLoc (m,0) & f . (IC ) = F₂(m) ) ) by A8;
take f ; :: thesis:
thus IC f = F₃() by A15, SCMPDS_2:52, SCMPDS_2:98; :: thesis:
let i be Element of NAT ; :: thesis:
A16: i in NAT ;
NAT c= the carrier of SCMPDS by COMPOS_1:def 2;
then i in the carrier of SCMPDS by A16;
then ex m being Element of NAT st
( ( i = IC & f . i = F₃() ) or ( i = m & f . i = F₁(m) ) or ( i = DataLoc (m,0) & f . i = F₂(m) ) ) by A8;
hence f . i = F₁(i) by SCMPDS_2:53, SCMPDS_2:98; :: thesis:
ex m being Element of NAT st
( ( DataLoc (i,0) = IC & f . (DataLoc (i,0)) = F₃() ) or ( DataLoc (i,0) = m & f . (DataLoc (i,0)) = F₁(m) ) or ( DataLoc (i,0) = DataLoc (m,0) & f . (DataLoc (i,0)) = F₂(m) ) ) by A8;
hence f . (DataLoc (i,0)) = F₂(i) by Th17, SCMPDS_2:52, SCMPDS_2:53; :: thesis: