A1:
ND (V,A) c= ND (V,A)
;

consider p being SCPartialNominativePredicate of V,A such that

A2: ( dom p = ND (V,A) & ( 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 = ND (V,A) & ( for d being object st d in dom p holds

( ( factorial_inv_pred A,loc,n0,d implies p . d = TRUE ) & ( not factorial_inv_pred A,loc,n0,d implies p . d = FALSE ) ) ) )

thus ( dom p = ND (V,A) & ( for d being object st d in dom p holds

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

consider p being SCPartialNominativePredicate of V,A such that

A2: ( dom p = ND (V,A) & ( for d being object st d in dom p holds

( ( S

take p ; :: thesis: ( dom p = ND (V,A) & ( for d being object st d in dom p holds

( ( factorial_inv_pred A,loc,n0,d implies p . d = TRUE ) & ( not factorial_inv_pred A,loc,n0,d implies p . d = FALSE ) ) ) )

thus ( dom p = ND (V,A) & ( for d being object st d in dom p holds

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