set F = SCM*-VAL * SCM+FSA-OK;
let n be object ; :: according to FUNCT_1:def 9 :: thesis: ( not n in proj1 (SCM*-VAL * SCM+FSA-OK) or not (SCM*-VAL * SCM+FSA-OK) . n is empty )
assume A1: n in dom (SCM*-VAL * SCM+FSA-OK) ; :: thesis: not (SCM*-VAL * SCM+FSA-OK) . n is empty
dom (SCM*-VAL * SCM+FSA-OK) = SCM+FSA-Memory by Lm8;
then ( n in SCM-Memory or n in SCM+FSA-Data*-Loc ) by A1, XBOOLE_0:def 3;

per cases then ( n = NAT or n in SCM-Data-Loc or n in SCM+FSA-Data*-Loc ) by AMI_2:26;

suppose n = NAT ; :: thesis: not (SCM*-VAL * SCM+FSA-OK) . n is empty

then (SCM*-VAL * SCM+FSA-OK) . n = NAT by Th4;
hence not (SCM*-VAL * SCM+FSA-OK) . n is empty ; :: thesis: verum

end;

suppose n in SCM-Data-Loc ; :: thesis: not (SCM*-VAL * SCM+FSA-OK) . n is empty

then (SCM*-VAL * SCM+FSA-OK) . n = INT by Th5;
hence not (SCM*-VAL * SCM+FSA-OK) . n is empty ; :: thesis: verum

end;

suppose n in SCM+FSA-Data*-Loc ; :: thesis: not (SCM*-VAL * SCM+FSA-OK) . n is empty

then (SCM*-VAL * SCM+FSA-OK) . n = INT * by Th6;
hence not (SCM*-VAL * SCM+FSA-OK) . n is empty ; :: thesis: verum

end;

end;