let V, A be set ; :: thesis: for p being SCPartialNominativePredicate of V,A
for E being V,A -FPrg-yielding FinSequence
for e being Element of product E st product E <> {} holds
<*(SC_Psuperpos (p,e,E)),(SC_Fsuperpos ((PPid (ND (V,A))),e,E)),p*> is SFHT of (ND (V,A))
let p be SCPartialNominativePredicate of V,A; :: thesis: for E being V,A -FPrg-yielding FinSequence
for e being Element of product E st product E <> {} holds
<*(SC_Psuperpos (p,e,E)),(SC_Fsuperpos ((PPid (ND (V,A))),e,E)),p*> is SFHT of (ND (V,A))
let E be V,A -FPrg-yielding FinSequence; :: thesis: for e being Element of product E st product E <> {} holds
<*(SC_Psuperpos (p,e,E)),(SC_Fsuperpos ((PPid (ND (V,A))),e,E)),p*> is SFHT of (ND (V,A))
let e be Element of product E; :: thesis: ( product E <> {} implies <*(SC_Psuperpos (p,e,E)),(SC_Fsuperpos ((PPid (ND (V,A))),e,E)),p*> is SFHT of (ND (V,A)) )
assume A1: product E <> {} ; :: thesis: <*(SC_Psuperpos (p,e,E)),(SC_Fsuperpos ((PPid (ND (V,A))),e,E)),p*> is SFHT of (ND (V,A))
set I = PPid (ND (V,A));
set P = SC_Psuperpos (p,e,E);
set F = SC_Fsuperpos ((PPid (ND (V,A))),e,E);
for d being TypeSCNominativeData of V,A st d in dom (SC_Psuperpos (p,e,E)) & (SC_Psuperpos (p,e,E)) . d = TRUE & d in dom (SC_Fsuperpos ((PPid (ND (V,A))),e,E)) & (SC_Fsuperpos ((PPid (ND (V,A))),e,E)) . d in dom p holds
p . ((SC_Fsuperpos ((PPid (ND (V,A))),e,E)) . d) = TRUE

proof

let d be TypeSCNominativeData of V,A; :: thesis: ( d in dom (SC_Psuperpos (p,e,E)) & (SC_Psuperpos (p,e,E)) . d = TRUE & d in dom (SC_Fsuperpos ((PPid (ND (V,A))),e,E)) & (SC_Fsuperpos ((PPid (ND (V,A))),e,E)) . d in dom p implies p . ((SC_Fsuperpos ((PPid (ND (V,A))),e,E)) . d) = TRUE )
assume that
A2: d in dom (SC_Psuperpos (p,e,E)) and
A3: (SC_Psuperpos (p,e,E)) . d = TRUE and
A4: d in dom (SC_Fsuperpos ((PPid (ND (V,A))),e,E)) and
(SC_Fsuperpos ((PPid (ND (V,A))),e,E)) . d in dom p ; :: thesis: p . ((SC_Fsuperpos ((PPid (ND (V,A))),e,E)) . d) = TRUE
set X = E;
set o = global_overlapping (V,A,d,(NDentry (E,E,d)));
global_overlapping (V,A,d,(NDentry (E,E,d))) in ND (V,A) ;
then global_overlapping (V,A,d,(NDentry (E,E,d))) = (PPid (ND (V,A))) . (global_overlapping (V,A,d,(NDentry (E,E,d)))) by FUNCT_1:18
.= (SC_Fsuperpos ((PPid (ND (V,A))),e,E)) . d by A1, A4, NOMIN_2:37 ;
hence p . ((SC_Fsuperpos ((PPid (ND (V,A))),e,E)) . d) = TRUE by A1, A2, A3, NOMIN_2:34; :: thesis: verum

end;

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