A1:
{ d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } c= ND (V,A)
proof
let v be
object ;
TARSKI:def 3 ( not v in { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } or v in ND (V,A) )
assume
v in { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) }
;
v in ND (V,A)
then
ex
d being
TypeSCNominativeData of
V,
A st
(
v = d &
d in dom (denaming (V,A,z)) )
;
hence
v in ND (
V,
A)
;
verum
end;
consider p being SCPartialNominativePredicate of V,A such that
A2:
( 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
( ( S1[d] implies p . d = TRUE ) & ( not S1[d] implies p . d = FALSE ) ) ) )
from PARTPR_2:sch 1(A1);
take
p
; ( 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
( ( valid_power_output_pred A,z,b0,n0,d implies p . d = TRUE ) & ( not valid_power_output_pred A,z,b0,n0,d implies p . d = FALSE ) ) ) )
thus
( 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
( ( valid_power_output_pred A,z,b0,n0,d implies p . d = TRUE ) & ( not valid_power_output_pred A,z,b0,n0,d implies p . d = FALSE ) ) ) )
by A2; verum