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_Fsuperpos ((PPid (ND (V,A))),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_Fsuperpos ((PPid (ND (V,A))),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_Fsuperpos ((PPid (ND (V,A))),f,v)),p*> is SFHT of (ND (V,A))
let f be SCBinominativeFunction of V,A; :: thesis: <*(SC_Psuperpos (p,f,v)),(SC_Fsuperpos ((PPid (ND (V,A))),f,v)),p*> is SFHT of (ND (V,A))
set I = PPid (ND (V,A));
set P = SC_Psuperpos (p,f,v);
set F = SC_Fsuperpos ((PPid (ND (V,A))),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_Fsuperpos ((PPid (ND (V,A))),f,v)) & (SC_Fsuperpos ((PPid (ND (V,A))),f,v)) . d in dom p holds
p . ((SC_Fsuperpos ((PPid (ND (V,A))),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_Fsuperpos ((PPid (ND (V,A))),f,v)) & (SC_Fsuperpos ((PPid (ND (V,A))),f,v)) . d in dom p implies p . ((SC_Fsuperpos ((PPid (ND (V,A))),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_Fsuperpos ((PPid (ND (V,A))),f,v)) and
(SC_Fsuperpos ((PPid (ND (V,A))),f,v)) . d in dom p ; :: thesis: p . ((SC_Fsuperpos ((PPid (ND (V,A))),f,v)) . d) = TRUE
set o = local_overlapping (V,A,d,(f . d),v);
local_overlapping (V,A,d,(f . d),v) in ND (V,A) ;
then local_overlapping (V,A,d,(f . d),v) = (PPid (ND (V,A))) . (local_overlapping (V,A,d,(f . d),v)) by FUNCT_1:18
.= (SC_Fsuperpos ((PPid (ND (V,A))),f,v)) . d by A2, NOMIN_2:38 ;
hence p . ((SC_Fsuperpos ((PPid (ND (V,A))),f,v)) . d) = TRUE by A1, NOMIN_2:35; :: thesis: verum

end;

hence <*(SC_Psuperpos (p,f,v)),(SC_Fsuperpos ((PPid (ND (V,A))),f,v)),p*> is SFHT of (ND (V,A)) by Th27; :: thesis: verum