set F = (SCM-VAL G) * SCM-OK;
let n be object ; :: according to FUNCT_1:def 9 :: thesis: ( not n in proj1 ((SCM-VAL G) * SCM-OK) or not ((SCM-VAL G) * SCM-OK) . n is empty )
assume A1: n in dom ((SCM-VAL G) * SCM-OK) ; :: thesis: not ((SCM-VAL G) * SCM-OK) . n is empty
dom ((SCM-VAL G) * SCM-OK) = SCM-Memory by Lm1;

per cases then ( n = NAT or n in SCM-Data-Loc ) by A1, AMI_2:26;

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

((SCM-VAL G) * SCM-OK) . n = NAT by A2, Th1;
hence not ((SCM-VAL G) * SCM-OK) . n is empty ; :: thesis: verum

end;

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

then ((SCM-VAL G) * SCM-OK) . n = the carrier of G by Th2;
hence not ((SCM-VAL G) * SCM-OK) . n is empty ; :: thesis: verum

end;

end;