A1:
{ d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } c= ND (V,A)

A2: ( dom p = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being object st d in dom p holds

( ( S_{1}[d] implies p . d = TRUE ) & ( not S_{1}[d] implies p . d = FALSE ) ) ) )
from PARTPR_2:sch 1(A1);

take p ; :: thesis: ( dom p = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being object st d in dom p holds

( ( valid_factorial_output_pred A,z,n0,d implies p . d = TRUE ) & ( not valid_factorial_output_pred A,z,n0,d implies p . d = FALSE ) ) ) )

thus ( dom p = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being object st d in dom p holds

( ( valid_factorial_output_pred A,z,n0,d implies p . d = TRUE ) & ( not valid_factorial_output_pred A,z,n0,d implies p . d = FALSE ) ) ) ) by A2; :: thesis: verum

proof

consider p being SCPartialNominativePredicate of V,A such that
let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } or v in ND (V,A) )

assume v in { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } ; :: thesis: v in ND (V,A)

then ex d being TypeSCNominativeData of V,A st

( v = d & d in dom (denaming (V,A,z)) ) ;

hence v in ND (V,A) ; :: thesis: verum

end;assume v in { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } ; :: thesis: v in ND (V,A)

then ex d being TypeSCNominativeData of V,A st

( v = d & d in dom (denaming (V,A,z)) ) ;

hence v in ND (V,A) ; :: thesis: verum

A2: ( dom p = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being object st d in dom p holds

( ( S

take p ; :: thesis: ( dom p = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being object st d in dom p holds

( ( valid_factorial_output_pred A,z,n0,d implies p . d = TRUE ) & ( not valid_factorial_output_pred A,z,n0,d implies p . d = FALSE ) ) ) )

thus ( dom p = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being object st d in dom p holds

( ( valid_factorial_output_pred A,z,n0,d implies p . d = TRUE ) & ( not valid_factorial_output_pred A,z,n0,d implies p . d = FALSE ) ) ) ) by A2; :: thesis: verum