let v be object ; :: thesis: for V, A being set
for p, q being SCPartialNominativePredicate of V,A
for f, g being SCBinominativeFunction of V,A st <*p,(PP_composition ((SC_Fsuperpos ((PPid (ND (V,A))),g,v)),f)),q*> is SFHT of (ND (V,A)) holds
<*p,(SC_Fsuperpos (f,g,v)),q*> is SFHT of (ND (V,A))
let V, A be set ; :: thesis: for p, q being SCPartialNominativePredicate of V,A
for f, g being SCBinominativeFunction of V,A st <*p,(PP_composition ((SC_Fsuperpos ((PPid (ND (V,A))),g,v)),f)),q*> is SFHT of (ND (V,A)) holds
<*p,(SC_Fsuperpos (f,g,v)),q*> is SFHT of (ND (V,A))
let p, q be SCPartialNominativePredicate of V,A; :: thesis: for f, g being SCBinominativeFunction of V,A st <*p,(PP_composition ((SC_Fsuperpos ((PPid (ND (V,A))),g,v)),f)),q*> is SFHT of (ND (V,A)) holds
<*p,(SC_Fsuperpos (f,g,v)),q*> is SFHT of (ND (V,A))
let f, g be SCBinominativeFunction of V,A; :: thesis: ( <*p,(PP_composition ((SC_Fsuperpos ((PPid (ND (V,A))),g,v)),f)),q*> is SFHT of (ND (V,A)) implies <*p,(SC_Fsuperpos (f,g,v)),q*> is SFHT of (ND (V,A)) )
set I = PPid (ND (V,A));
set F = SC_Fsuperpos (f,g,v);
set G = SC_Fsuperpos ((PPid (ND (V,A))),g,v);
set C = PP_composition ((SC_Fsuperpos ((PPid (ND (V,A))),g,v)),f);
assume <*p,(PP_composition ((SC_Fsuperpos ((PPid (ND (V,A))),g,v)),f)),q*> is SFHT of (ND (V,A)) ; :: thesis: <*p,(SC_Fsuperpos (f,g,v)),q*> is SFHT of (ND (V,A))
then A1: 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))),g,v)),f)) & (PP_composition ((SC_Fsuperpos ((PPid (ND (V,A))),g,v)),f)) . d in dom q holds
q . ((PP_composition ((SC_Fsuperpos ((PPid (ND (V,A))),g,v)),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,g,v)) & (SC_Fsuperpos (f,g,v)) . d in dom q holds
q . ((SC_Fsuperpos (f,g,v)) . d) = TRUE
proof
let d be TypeSCNominativeData of V,A; :: thesis: ( d in dom p & p . d = TRUE & d in dom (SC_Fsuperpos (f,g,v)) & (SC_Fsuperpos (f,g,v)) . d in dom q implies q . ((SC_Fsuperpos (f,g,v)) . d) = TRUE )
assume that
A2: d in dom p and
A3: p . d = TRUE and
A4: d in dom (SC_Fsuperpos (f,g,v)) and
A5: (SC_Fsuperpos (f,g,v)) . d in dom q ; :: thesis: q . ((SC_Fsuperpos (f,g,v)) . d) = TRUE
set o = local_overlapping (V,A,d,(g . d),v);
A6: (SC_Fsuperpos (f,g,v)) . d = f . (local_overlapping (V,A,d,(g . d),v)) by A4, NOMIN_2:38;
A7: local_overlapping (V,A,d,(g . d),v) in ND (V,A) ;
dom (SC_Fsuperpos (f,g,v)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,(g . d),v) in dom f & d in dom g ) } by NOMIN_2:def 15;
then consider d1 being TypeSCNominativeData of V,A such that
A8: d = d1 and
A9: local_overlapping (V,A,d1,(g . d1),v) in dom f and
A10: d1 in dom g by A4;
dom (SC_Fsuperpos ((PPid (ND (V,A))),g,v)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,(g . d),v) in dom (PPid (ND (V,A))) & d in dom g ) } by NOMIN_2:def 15;
then A11: d in dom (SC_Fsuperpos ((PPid (ND (V,A))),g,v)) by A7, A8, A10;
A12: local_overlapping (V,A,d,(g . d),v) = (PPid (ND (V,A))) . (local_overlapping (V,A,d,(g . d),v)) by A7, FUNCT_1:18
.= (SC_Fsuperpos ((PPid (ND (V,A))),g,v)) . d by A11, NOMIN_2:38 ;
A13: PP_composition ((SC_Fsuperpos ((PPid (ND (V,A))),g,v)),f) = f * (SC_Fsuperpos ((PPid (ND (V,A))),g,v)) by PARTPR_2:def 1;
then (PP_composition ((SC_Fsuperpos ((PPid (ND (V,A))),g,v)),f)) . d = f . ((SC_Fsuperpos ((PPid (ND (V,A))),g,v)) . d) by A11, FUNCT_1:13;
hence q . ((SC_Fsuperpos (f,g,v)) . d) = TRUE by A1, A2, A3, A5, A6, A11, A13, A8, A9, A12, FUNCT_1:11; :: thesis: verum
end;
hence <*p,(SC_Fsuperpos (f,g,v)),q*> is SFHT of (ND (V,A)) by Th27; :: thesis: verum