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_{1}[d] implies p . d = TRUE ) & ( not S_{1}[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_{1}[d] implies q . d = TRUE ) & ( not S_{1}[d] implies q . d = FALSE ) ) ) holds

p = q from PARTPR_2:sch 2();

hence for b_{1}, b_{2} being SCPartialNominativePredicate of V,A st dom b_{1} = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being object st d in dom b_{1} holds

( ( valid_factorial_output_pred A,z,n0,d implies b_{1} . d = TRUE ) & ( not valid_factorial_output_pred A,z,n0,d implies b_{1} . d = FALSE ) ) ) & dom b_{2} = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being object st d in dom b_{2} holds

( ( valid_factorial_output_pred A,z,n0,d implies b_{2} . d = TRUE ) & ( not valid_factorial_output_pred A,z,n0,d implies b_{2} . d = FALSE ) ) ) holds

b_{1} = b_{2}
; :: thesis: verum

( ( S

( ( S

p = q from PARTPR_2:sch 2();

hence for b

( ( valid_factorial_output_pred A,z,n0,d implies b

( ( valid_factorial_output_pred A,z,n0,d implies b

b