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
( ( S₁[d] implies p . d = TRUE ) & ( not S₁[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_Fibonacci_output_pred A,z,n0,d implies p . d = TRUE ) & ( not valid_Fibonacci_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_Fibonacci_output_pred A,z,n0,d implies p . d = TRUE ) & ( not valid_Fibonacci_output_pred A,z,n0,d implies p . d = FALSE ) ) ) ) by A2; :: thesis: verum