A1: { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } c= ND (V,A)
proof
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;
consider p being SCPartialNominativePredicate of V,A such that
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
( ( S1[d] implies p . d = TRUE ) & ( not S1[d] implies p . d = FALSE ) ) ) ) from 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