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

let e be object ; :: thesis:
assume e in the carrier of SCMPDS ; :: thesis:
then A2: e in {(IC )} \/ SCM-Data-Loc by SCMPDS_2:84, STRUCT_0:4;

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 AMI_2:def 16;
hence ex m being Nat st e = DataLoc (m,0) by Th4; :: thesis:

end;

end;

end;

then consider m being Nat such that
A3: ( e = IC 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 = DataLoc (m,0) ; :: thesis:

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

end;

end;

end;

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

let x be object ; :: thesis:
assume A9: x in dom the Object-Kind of SCMPDS ; :: thesis:
then A10: x in {(IC )} \/ SCM-Data-Loc by A8, SCMPDS_2:84, STRUCT_0:4;
consider m being Nat such that
A11: ( ( x = IC & f . x = F₂() ) or ( x = DataLoc (m,0) & f . x = F₁(m) ) ) by A7, A8, A9;

per cases by A10, XBOOLE_0:def 3;

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

then x is Int_position by AMI_2:def 16;
then (the_Values_of SCMPDS) . x = Values (DataLoc (m,0)) by A11, SCMPDS_2:43
.= INT by SCMPDS_2:5 ;
hence f . x in (the_Values_of SCMPDS) . x by A11, INT_1:def 2; :: thesis:

end;

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

(the_Values_of SCMPDS) . x = Values (IC ) by TARSKI:def 1, A12
.= NAT by MEMSTR_0:def 6 ;
hence f . x in (the_Values_of SCMPDS) . x by A11, A12, SCMPDS_2:2, TARSKI:def 1; :: thesis:

end;

end;

end;

then reconsider f = f as State of SCMPDS by A6, A8, FUNCT_1:def 14, PARTFUN1:def 2, RELAT_1:def 18;
consider m being Nat such that
A13: ( ( IC = IC & f . (IC ) = F₂() ) or ( IC = DataLoc (m,0) & f . (IC ) = F₁(m) ) ) by A7;
take f ; :: thesis:
thus IC f = F₂() by A13, SCMPDS_2:43; :: thesis:
let i be Nat; :: thesis:
ex m being Nat st
( ( DataLoc (i,0) = IC & f . (DataLoc (i,0)) = F₂() ) or ( DataLoc (i,0) = DataLoc (m,0) & f . (DataLoc (i,0)) = F₁(m) ) ) by A7;
hence f . (DataLoc (i,0)) = F₁(i) by Th3, SCMPDS_2:43; :: thesis: