let V, A be set ; :: thesis: for a being Element of V
for x being object
for p being SCPartialNominativePredicate of V,A holds <*(PP_inversion (SC_Psuperpos (p,(denaming (V,A,x)),a))),(SC_assignment ((denaming (V,A,x)),a)),p*> is SFHT of (ND (V,A))
let a be Element of V; :: thesis: for x being object
for p being SCPartialNominativePredicate of V,A holds <*(PP_inversion (SC_Psuperpos (p,(denaming (V,A,x)),a))),(SC_assignment ((denaming (V,A,x)),a)),p*> is SFHT of (ND (V,A))
let x be object ; :: thesis: for p being SCPartialNominativePredicate of V,A holds <*(PP_inversion (SC_Psuperpos (p,(denaming (V,A,x)),a))),(SC_assignment ((denaming (V,A,x)),a)),p*> is SFHT of (ND (V,A))
let p be SCPartialNominativePredicate of V,A; :: thesis: <*(PP_inversion (SC_Psuperpos (p,(denaming (V,A,x)),a))),(SC_assignment ((denaming (V,A,x)),a)),p*> is SFHT of (ND (V,A))
set Dx = denaming (V,A,x);
set F = SC_assignment ((denaming (V,A,x)),a);
set P = SC_Psuperpos (p,(denaming (V,A,x)),a);
set I = PP_inversion (SC_Psuperpos (p,(denaming (V,A,x)),a));
for d being TypeSCNominativeData of V,A st d in dom (PP_inversion (SC_Psuperpos (p,(denaming (V,A,x)),a))) & (PP_inversion (SC_Psuperpos (p,(denaming (V,A,x)),a))) . d = TRUE & d in dom (SC_assignment ((denaming (V,A,x)),a)) & (SC_assignment ((denaming (V,A,x)),a)) . d in dom p holds
p . ((SC_assignment ((denaming (V,A,x)),a)) . d) = TRUE
proof
let d be TypeSCNominativeData of V,A; :: thesis: ( d in dom (PP_inversion (SC_Psuperpos (p,(denaming (V,A,x)),a))) & (PP_inversion (SC_Psuperpos (p,(denaming (V,A,x)),a))) . d = TRUE & d in dom (SC_assignment ((denaming (V,A,x)),a)) & (SC_assignment ((denaming (V,A,x)),a)) . d in dom p implies p . ((SC_assignment ((denaming (V,A,x)),a)) . d) = TRUE )
assume that
A1: d in dom (PP_inversion (SC_Psuperpos (p,(denaming (V,A,x)),a))) and
(PP_inversion (SC_Psuperpos (p,(denaming (V,A,x)),a))) . d = TRUE and
A2: d in dom (SC_assignment ((denaming (V,A,x)),a)) and
A3: (SC_assignment ((denaming (V,A,x)),a)) . d in dom p ; :: thesis: p . ((SC_assignment ((denaming (V,A,x)),a)) . d) = TRUE
dom (PP_inversion (SC_Psuperpos (p,(denaming (V,A,x)),a))) = { d where d is Element of ND (V,A) : not d in dom (SC_Psuperpos (p,(denaming (V,A,x)),a)) } by PARTPR_2:def 17;
then A4: ex d1 being Element of ND (V,A) st
( d1 = d & not d1 in dom (SC_Psuperpos (p,(denaming (V,A,x)),a)) ) by A1;
dom (SC_assignment ((denaming (V,A,x)),a)) = dom (denaming (V,A,x)) by NOMIN_2:def 7;
then SC_Psuperpos (p,(denaming (V,A,x)),a),d =~ p, local_overlapping (V,A,d,((denaming (V,A,x)) . d),a) by A2, NOMIN_2:def 11;
hence p . ((SC_assignment ((denaming (V,A,x)),a)) . d) = TRUE by A2, A3, A4, NOMIN_2:def 7; :: thesis: verum
end;
hence <*(PP_inversion (SC_Psuperpos (p,(denaming (V,A,x)),a))),(SC_assignment ((denaming (V,A,x)),a)),p*> is SFHT of (ND (V,A)) by NOMIN_3:28; :: thesis: verum