let V, A be set ; for p, q being SCPartialNominativePredicate of V,A
for f being SCBinominativeFunction of V,A
for E being V,A -FPrg-yielding FinSequence
for e being Element of product E st product E <> {} & <*p,(PP_composition ((SC_Fsuperpos ((PPid (ND (V,A))),e,E)),f)),q*> is SFHT of (ND (V,A)) holds
<*p,(SC_Fsuperpos (f,e,E)),q*> is SFHT of (ND (V,A))
let p, q be SCPartialNominativePredicate of V,A; for f being SCBinominativeFunction of V,A
for E being V,A -FPrg-yielding FinSequence
for e being Element of product E st product E <> {} & <*p,(PP_composition ((SC_Fsuperpos ((PPid (ND (V,A))),e,E)),f)),q*> is SFHT of (ND (V,A)) holds
<*p,(SC_Fsuperpos (f,e,E)),q*> is SFHT of (ND (V,A))
let f be SCBinominativeFunction of V,A; for E being V,A -FPrg-yielding FinSequence
for e being Element of product E st product E <> {} & <*p,(PP_composition ((SC_Fsuperpos ((PPid (ND (V,A))),e,E)),f)),q*> is SFHT of (ND (V,A)) holds
<*p,(SC_Fsuperpos (f,e,E)),q*> is SFHT of (ND (V,A))
let E be V,A -FPrg-yielding FinSequence; for e being Element of product E st product E <> {} & <*p,(PP_composition ((SC_Fsuperpos ((PPid (ND (V,A))),e,E)),f)),q*> is SFHT of (ND (V,A)) holds
<*p,(SC_Fsuperpos (f,e,E)),q*> is SFHT of (ND (V,A))
let e be Element of product E; ( product E <> {} & <*p,(PP_composition ((SC_Fsuperpos ((PPid (ND (V,A))),e,E)),f)),q*> is SFHT of (ND (V,A)) implies <*p,(SC_Fsuperpos (f,e,E)),q*> is SFHT of (ND (V,A)) )
assume A1:
product E <> {}
; ( not <*p,(PP_composition ((SC_Fsuperpos ((PPid (ND (V,A))),e,E)),f)),q*> is SFHT of (ND (V,A)) or <*p,(SC_Fsuperpos (f,e,E)),q*> is SFHT of (ND (V,A)) )
set I = PPid (ND (V,A));
set F = SC_Fsuperpos (f,e,E);
set G = SC_Fsuperpos ((PPid (ND (V,A))),e,E);
set C = PP_composition ((SC_Fsuperpos ((PPid (ND (V,A))),e,E)),f);
assume
<*p,(PP_composition ((SC_Fsuperpos ((PPid (ND (V,A))),e,E)),f)),q*> is SFHT of (ND (V,A))
; <*p,(SC_Fsuperpos (f,e,E)),q*> is SFHT of (ND (V,A))
then A2:
for d being TypeSCNominativeData of V,A st d in dom p & p . d = TRUE & d in dom (PP_composition ((SC_Fsuperpos ((PPid (ND (V,A))),e,E)),f)) & (PP_composition ((SC_Fsuperpos ((PPid (ND (V,A))),e,E)),f)) . d in dom q holds
q . ((PP_composition ((SC_Fsuperpos ((PPid (ND (V,A))),e,E)),f)) . d) = TRUE
by Th11;
for d being TypeSCNominativeData of V,A st d in dom p & p . d = TRUE & d in dom (SC_Fsuperpos (f,e,E)) & (SC_Fsuperpos (f,e,E)) . d in dom q holds
q . ((SC_Fsuperpos (f,e,E)) . d) = TRUE
proof
let d be
TypeSCNominativeData of
V,
A;
( d in dom p & p . d = TRUE & d in dom (SC_Fsuperpos (f,e,E)) & (SC_Fsuperpos (f,e,E)) . d in dom q implies q . ((SC_Fsuperpos (f,e,E)) . d) = TRUE )
assume that A3:
d in dom p
and A4:
p . d = TRUE
and A5:
d in dom (SC_Fsuperpos (f,e,E))
and A6:
(SC_Fsuperpos (f,e,E)) . d in dom q
;
q . ((SC_Fsuperpos (f,e,E)) . d) = TRUE
set X =
E;
set o =
global_overlapping (
V,
A,
d,
(NDentry (E,E,d)));
A7:
global_overlapping (
V,
A,
d,
(NDentry (E,E,d)))
in ND (
V,
A)
;
SC_Fsuperpos (
f,
e,
E)
= (SCFsuperpos (E,E)) . (
f,
e)
by A1, NOMIN_2:def 14;
then
dom (SC_Fsuperpos (f,e,E)) = { d where d is TypeSCNominativeData of V,A : ( global_overlapping (V,A,d,(NDentry (E,E,d))) in dom f & d in_doms E ) }
by A1, NOMIN_2:def 13;
then consider d1 being
TypeSCNominativeData of
V,
A such that A8:
d = d1
and A9:
global_overlapping (
V,
A,
d1,
(NDentry (E,E,d1)))
in dom f
and A10:
d1 in_doms E
by A5;
SC_Fsuperpos (
(PPid (ND (V,A))),
e,
E)
= (SCFsuperpos (E,E)) . (
(PPid (ND (V,A))),
e)
by A1, NOMIN_2:def 14;
then
dom (SC_Fsuperpos ((PPid (ND (V,A))),e,E)) = { d where d is TypeSCNominativeData of V,A : ( global_overlapping (V,A,d,(NDentry (E,E,d))) in dom (PPid (ND (V,A))) & d in_doms E ) }
by A1, NOMIN_2:def 13;
then A11:
d in dom (SC_Fsuperpos ((PPid (ND (V,A))),e,E))
by A7, A8, A10;
A12:
(SC_Fsuperpos (f,e,E)) . d = f . (global_overlapping (V,A,d,(NDentry (E,E,d))))
by A1, A5, NOMIN_2:37;
A13:
global_overlapping (
V,
A,
d,
(NDentry (E,E,d))) =
(PPid (ND (V,A))) . (global_overlapping (V,A,d,(NDentry (E,E,d))))
by A7, FUNCT_1:18
.=
(SC_Fsuperpos ((PPid (ND (V,A))),e,E)) . d
by A1, A11, NOMIN_2:37
;
A14:
PP_composition (
(SC_Fsuperpos ((PPid (ND (V,A))),e,E)),
f)
= f * (SC_Fsuperpos ((PPid (ND (V,A))),e,E))
by PARTPR_2:def 1;
then
(PP_composition ((SC_Fsuperpos ((PPid (ND (V,A))),e,E)),f)) . d = f . ((SC_Fsuperpos ((PPid (ND (V,A))),e,E)) . d)
by A11, FUNCT_1:13;
hence
q . ((SC_Fsuperpos (f,e,E)) . d) = TRUE
by A2, A3, A4, A6, A12, A11, A14, A8, A9, A13, FUNCT_1:11;
verum
end;
hence
<*p,(SC_Fsuperpos (f,e,E)),q*> is SFHT of (ND (V,A))
by Th27; verum