for p, q being SCPartialNominativePredicate of V,A st dom p = ND (V,A) & ( for d being object st d in dom p holds
( ( S1[d] implies p . d = TRUE ) & ( not S1[d] implies p . d = FALSE ) ) ) & dom q = ND (V,A) & ( for d being object st d in dom q holds
( ( S1[d] implies q . d = TRUE ) & ( not S1[d] implies q . d = FALSE ) ) ) holds
p = q
from PARTPR_2:sch 2();
hence
for b1, b2 being SCPartialNominativePredicate of V,A st dom b1 = ND (V,A) & ( for d being object st d in dom b1 holds
( ( factorial_inv_pred A,loc,n0,d implies b1 . d = TRUE ) & ( not factorial_inv_pred A,loc,n0,d implies b1 . d = FALSE ) ) ) & dom b2 = ND (V,A) & ( for d being object st d in dom b2 holds
( ( factorial_inv_pred A,loc,n0,d implies b2 . d = TRUE ) & ( not factorial_inv_pred A,loc,n0,d implies b2 . d = FALSE ) ) ) holds
b1 = b2
; verum