for p, q being SCPartialNominativePredicate of V,A st 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 ) ) ) & dom q = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being object st d in dom q holds
( ( S₁[d] implies q . d = TRUE ) & ( not S₁[d] implies q . d = FALSE ) ) ) holds
p = q from PARTPR_2:sch 2();
hence for b₁, b₂ being SCPartialNominativePredicate of V,A st dom b₁ = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being object st d in dom b₁ holds
( ( valid_factorial_output_pred A,z,n0,d implies b₁ . d = TRUE ) & ( not valid_factorial_output_pred A,z,n0,d implies b₁ . d = FALSE ) ) ) & dom b₂ = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being object st d in dom b₂ holds
( ( valid_factorial_output_pred A,z,n0,d implies b₂ . d = TRUE ) & ( not valid_factorial_output_pred A,z,n0,d implies b₂ . d = FALSE ) ) ) holds
b₁ = b₂ ; :: thesis: verum