set S1 = {(IC SCMPDS )};
set S2 = SCM-Data-Loc ;
set S3 = NAT ;
defpred S₁[ set , set ] means ex m being Element of NAT st
( ( $1 = IC SCMPDS & $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 A2: ( e in {(IC SCMPDS )} \/ SCM-Data-Loc or e in NAT ) by SCMPDS_3:5, XBOOLE_0:def 3;

now

per cases by A2, XBOOLE_0:def 3;

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

hence e = IC SCMPDS 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 SCMPDS or e = m or e = DataLoc m,0 ) ;

per cases by A3;

suppose A4: e = IC SCMPDS ; :: 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 A11: ( x in {(IC SCMPDS )} \/ SCM-Data-Loc or x in NAT ) by A9, SCMPDS_3:5, XBOOLE_0:def 3;
consider m being Element of NAT such that
A12: ( ( x = IC SCMPDS & 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 SCMPDS )} ; :: thesis:

then the Object-Kind of SCMPDS . x = ObjectKind (IC SCMPDS ) by TARSKI:def 1
.= NAT by AMI_1:def 11 ;
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 Object-Kind of SCMPDS . m by A12, AMI_1:48, SCMPDS_2:53
.= the Instructions of SCMPDS by AMI_1:def 14 ;
hence f . x in the Object-Kind of SCMPDS . x by A12, AMI_1:48, 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 SCMPDS = IC SCMPDS & f . (IC SCMPDS ) = F₃() ) or ( IC SCMPDS = m & f . (IC SCMPDS ) = F₁(m) ) or ( IC SCMPDS = DataLoc m,0 & f . (IC SCMPDS ) = F₂(m) ) ) by A8;
take f ; :: thesis:
m <> IC SCMPDS by SCMPDS_2:98;
hence IC f = F₃() by A15, SCMPDS_2:52; :: thesis:
let i be Element of NAT ; :: thesis:
A16: i <> IC SCMPDS by SCMPDS_2:98;
ex m being Element of NAT st
( ( i = IC SCMPDS & 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 A16, SCMPDS_2:53; :: thesis:
ex m being Element of NAT st
( ( DataLoc i,0 = IC SCMPDS & 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: