let v be object ; :: thesis: for V, A being set
for p being SCPartialNominativePredicate of V,A
for f being SCBinominativeFunction of V,A holds <*(SC_Psuperpos (p,f,v)),(SC_assignment (f,v)),p*> is SFHT of (ND (V,A))
let V, A be set ; :: thesis: for p being SCPartialNominativePredicate of V,A
for f being SCBinominativeFunction of V,A holds <*(SC_Psuperpos (p,f,v)),(SC_assignment (f,v)),p*> is SFHT of (ND (V,A))
let p be SCPartialNominativePredicate of V,A; :: thesis: for f being SCBinominativeFunction of V,A holds <*(SC_Psuperpos (p,f,v)),(SC_assignment (f,v)),p*> is SFHT of (ND (V,A))
let f be SCBinominativeFunction of V,A; :: thesis: <*(SC_Psuperpos (p,f,v)),(SC_assignment (f,v)),p*> is SFHT of (ND (V,A))
set P = SC_Psuperpos (p,f,v);
set F = SC_assignment (f,v);
for d being TypeSCNominativeData of V,A st d in dom (SC_Psuperpos (p,f,v)) & (SC_Psuperpos (p,f,v)) . d = TRUE & d in dom (SC_assignment (f,v)) & (SC_assignment (f,v)) . d in dom p holds
p . ((SC_assignment (f,v)) . d) = TRUE
proof
let d be TypeSCNominativeData of V,A; :: thesis: ( d in dom (SC_Psuperpos (p,f,v)) & (SC_Psuperpos (p,f,v)) . d = TRUE & d in dom (SC_assignment (f,v)) & (SC_assignment (f,v)) . d in dom p implies p . ((SC_assignment (f,v)) . d) = TRUE )
assume that
A1: ( d in dom (SC_Psuperpos (p,f,v)) & (SC_Psuperpos (p,f,v)) . d = TRUE ) and
A2: d in dom (SC_assignment (f,v)) and
(SC_assignment (f,v)) . d in dom p ; :: thesis: p . ((SC_assignment (f,v)) . d) = TRUE
(SC_assignment (f,v)) . d = local_overlapping (V,A,d,(f . d),v) by A2, NOMIN_2:def 7;
hence p . ((SC_assignment (f,v)) . d) = TRUE by A1, NOMIN_2:35; :: thesis: verum
end;
hence <*(SC_Psuperpos (p,f,v)),(SC_assignment (f,v)),p*> is SFHT of (ND (V,A)) by Th27; :: thesis: verum