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

per cases ( n = NAT or n in SCM-Data-Loc ) by A1, Lm1, Lm5;

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

hence not (SCM-VAL * SCM-OK) . n is empty by Th1; :: thesis: verum

end;

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

hence not (SCM-VAL * SCM-OK) . n is empty by Th2; :: thesis: verum

end;

end;