let v be object ; 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 ; 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; 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; <*(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;
( 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
;
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;
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; verum