defpred S₁[ set , set ] means ( ( $1 = NAT & $2 = NAT ) or ( $1 in SCM-Data-Loc & $2 = the carrier of S ) or ( $1 in NAT & $2 = SCM-Instr S ) );

A1: now

let k be Element of SCM-Memory ; :: thesis: ex b being Element of {the carrier of S} \/ {(SCM-Instr S),NAT } st S₁[k,b]
A2: {the carrier of S} \/ {(SCM-Instr S),NAT } = {the carrier of S,(SCM-Instr S),NAT } by ENUMSET1:42;
then A3: NAT in {the carrier of S} \/ {(SCM-Instr S),NAT } by ENUMSET1:def 1;
A4: ( S₁[k, NAT ] or S₁[k,the carrier of S] or S₁[k, SCM-Instr S] ) by Lm1;
( the carrier of S in {the carrier of S} \/ {(SCM-Instr S),NAT } & SCM-Instr S in {the carrier of S} \/ {(SCM-Instr S),NAT } ) by A2, ENUMSET1:def 1;
hence ex b being Element of {the carrier of S} \/ {(SCM-Instr S),NAT } st S₁[k,b] by A3, A4; :: thesis: verum

end;

consider h being Function of SCM-Memory ,({the carrier of S} \/ {(SCM-Instr S),NAT }) such that
A5: for a being Element of SCM-Memory holds S₁[a,h . a] from FUNCT_2:sch 3(A1);
take h ; :: thesis: for k being Element of SCM-Memory holds
( ( k = NAT implies h . k = NAT ) & ( k in SCM-Data-Loc implies h . k = the carrier of S ) & ( k in NAT implies h . k = SCM-Instr S ) )
let k be Element of SCM-Memory ; :: thesis: ( ( k = NAT implies h . k = NAT ) & ( k in SCM-Data-Loc implies h . k = the carrier of S ) & ( k in NAT implies h . k = SCM-Instr S ) )
A6: S₁[k,h . k] by A5;
hence ( k = NAT implies h . k = NAT ) by AMI_2:27; :: thesis: ( ( k in SCM-Data-Loc implies h . k = the carrier of S ) & ( k in NAT implies h . k = SCM-Instr S ) )
thus ( k in SCM-Data-Loc implies h . k = the carrier of S ) by A6, AMI_2:27, AMI_2:29, XBOOLE_0:3; :: thesis: ( k in NAT implies h . k = SCM-Instr S )
thus ( k in NAT implies h . k = SCM-Instr S ) by A6, AMI_2:29, XBOOLE_0:3; :: thesis: verum