let F, G be SCPartialNominativePredicate of V,A; :: thesis: ( dom F = (ND (V,A)) \ A & ( for d being NonatomicND of V,A st d in dom F holds
( ( denaming (v,d) in dom F implies F . d = TRUE ) & ( not denaming (v,d) in dom F implies F . d = FALSE ) ) ) & dom G = (ND (V,A)) \ A & ( for d being NonatomicND of V,A st d in dom G holds
( ( denaming (v,d) in dom G implies G . d = TRUE ) & ( not denaming (v,d) in dom G implies G . d = FALSE ) ) ) implies F = G )
assume that
A5: dom F = (ND (V,A)) \ A and
A6: for d being NonatomicND of V,A st d in dom F holds
( ( denaming (v,d) in dom F implies F . d = TRUE ) & ( not denaming (v,d) in dom F implies F . d = FALSE ) ) and
A7: dom G = (ND (V,A)) \ A and
A8: for d being NonatomicND of V,A st d in dom G holds
( ( denaming (v,d) in dom G implies G . d = TRUE ) & ( not denaming (v,d) in dom G implies G . d = FALSE ) ) ; :: thesis: F = G
thus dom F = dom G by A5, A7; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom F or F . b₁ = G . b₁ )
let x be object ; :: thesis: ( not x in dom F or F . x = G . x )
assume A9: x in dom F ; :: thesis: F . x = G . x
then reconsider d = x as NonatomicND of V,A by A5, NOMIN_1:43;

per cases ( denaming (v,d) in dom F or not denaming (v,d) in dom F ) ;

suppose A10: denaming (v,d) in dom F ; :: thesis: F . x = G . x

hence F . x = TRUE by A6, A9
.= G . x by A5, A7, A8, A9, A10 ;
:: thesis: verum

end;

suppose A11: not denaming (v,d) in dom F ; :: thesis: F . x = G . x

hence F . x = FALSE by A6, A9
.= G . x by A5, A7, A8, A9, A11 ;
:: thesis: verum

end;

end;