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;