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₁[d] implies p . d = TRUE ) & ( not S₁[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