let v be object ; :: thesis: for V, A being set holds SC_exists ((PP_BottomPred (ND (V,A))),v) = PP_BottomPred (ND (V,A))
let V, A be set ; :: thesis: SC_exists ((PP_BottomPred (ND (V,A))),v) = PP_BottomPred (ND (V,A))
set B = PP_BottomPred (ND (V,A));
set T = PP_True (ND (V,A));
set o = SC_exists ((PP_BottomPred (ND (V,A))),v);
thus dom (SC_exists ((PP_BottomPred (ND (V,A))),v)) = dom (PP_BottomPred (ND (V,A))) :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom (SC_exists ((PP_BottomPred (ND (V,A))),v)) or (SC_exists ((PP_BottomPred (ND (V,A))),v)) . b₁ = (PP_BottomPred (ND (V,A))) . b₁ )

proof

thus dom (SC_exists ((PP_BottomPred (ND (V,A))),v)) c= dom (PP_BottomPred (ND (V,A))) :: according to XBOOLE_0:def 10 :: thesis: dom (PP_BottomPred (ND (V,A))) c= dom (SC_exists ((PP_BottomPred (ND (V,A))),v))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (SC_exists ((PP_BottomPred (ND (V,A))),v)) or x in dom (PP_BottomPred (ND (V,A))) )
assume x in dom (SC_exists ((PP_BottomPred (ND (V,A))),v)) ; :: thesis: x in dom (PP_BottomPred (ND (V,A)))
then ( ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,x,d1,v) in dom (PP_BottomPred (ND (V,A))) & (PP_BottomPred (ND (V,A))) . (local_overlapping (V,A,x,d1,v)) = TRUE ) or for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,x,d1,v) in dom (PP_BottomPred (ND (V,A))) & (PP_BottomPred (ND (V,A))) . (local_overlapping (V,A,x,d1,v)) = FALSE ) ) by Th18;
hence x in dom (PP_BottomPred (ND (V,A))) ; :: thesis: verum

end;

thus dom (PP_BottomPred (ND (V,A))) c= dom (SC_exists ((PP_BottomPred (ND (V,A))),v)) ; :: thesis: verum

end;

let x be object ; :: thesis: ( not x in dom (SC_exists ((PP_BottomPred (ND (V,A))),v)) or (SC_exists ((PP_BottomPred (ND (V,A))),v)) . x = (PP_BottomPred (ND (V,A))) . x )
assume x in dom (SC_exists ((PP_BottomPred (ND (V,A))),v)) ; :: thesis: (SC_exists ((PP_BottomPred (ND (V,A))),v)) . x = (PP_BottomPred (ND (V,A))) . x
then ( ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,x,d1,v) in dom (PP_BottomPred (ND (V,A))) & (PP_BottomPred (ND (V,A))) . (local_overlapping (V,A,x,d1,v)) = TRUE ) or for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,x,d1,v) in dom (PP_BottomPred (ND (V,A))) & (PP_BottomPred (ND (V,A))) . (local_overlapping (V,A,x,d1,v)) = FALSE ) ) by Th18;
hence (SC_exists ((PP_BottomPred (ND (V,A))),v)) . x = (PP_BottomPred (ND (V,A))) . x ; :: thesis: verum