let V, A be set ; 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; 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; 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; ( 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 <> {}
; <*(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;
( 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
;
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;
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; verum