let V, A be set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 <> {} ; :: thesis: ( 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)) ; :: thesis: <*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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum
end;
hence <*p,(SC_Fsuperpos (f,e,E)),q*> is SFHT of (ND (V,A)) by Th27; :: thesis: verum