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;