let D be non empty set ; :: thesis: for f, g being BinominativeFunction of D
for p, q, r being PartialPredicate of D st <*p,f,q*> is SFHT of D & <*q,g,r*> is SFHT of D & f,g coincide_with q,r holds
<*p,(PP_composition (f,g)),r*> is SFHT of D
let f, g be BinominativeFunction of D; :: thesis: for p, q, r being PartialPredicate of D st <*p,f,q*> is SFHT of D & <*q,g,r*> is SFHT of D & f,g coincide_with q,r holds
<*p,(PP_composition (f,g)),r*> is SFHT of D
let p, q, r be PartialPredicate of D; :: thesis: ( <*p,f,q*> is SFHT of D & <*q,g,r*> is SFHT of D & f,g coincide_with q,r implies <*p,(PP_composition (f,g)),r*> is SFHT of D )
assume that
A1: <*p,f,q*> is SFHT of D and
A2: <*q,g,r*> is SFHT of D and
A3: f,g coincide_with q,r ; :: thesis: <*p,(PP_composition (f,g)),r*> is SFHT of D
set F = PP_composition (f,g);
for d being Element of D st d in dom p & p . d = TRUE & d in dom (PP_composition (f,g)) & (PP_composition (f,g)) . d in dom r holds
r . ((PP_composition (f,g)) . d) = TRUE

proof

let d be Element of D; :: thesis: ( d in dom p & p . d = TRUE & d in dom (PP_composition (f,g)) & (PP_composition (f,g)) . d in dom r implies r . ((PP_composition (f,g)) . d) = TRUE )
assume that
A4: d in dom p and
A5: p . d = TRUE and
A6: d in dom (PP_composition (f,g)) and
A7: (PP_composition (f,g)) . d in dom r ; :: thesis: r . ((PP_composition (f,g)) . d) = TRUE
A8: PP_composition (f,g) = g * f by PARTPR_2:def 1;
then A9: (PP_composition (f,g)) . d = g . (f . d) by A6, FUNCT_1:12;
dom (g * f) c= dom f by RELAT_1:25;
then A10: f . d is Element of D by A6, A8, PARTFUN1:4;
A11: f . d in dom g by A6, A8, FUNCT_1:11;
A12: d in dom f by A6, A8, FUNCT_1:11;
then f . d in rng f by FUNCT_1:def 3;
then A13: f . d in dom q by A3, A7, A9, A10;
then q . (f . d) = TRUE by A1, A4, A5, A12, Th11;
hence r . ((PP_composition (f,g)) . d) = TRUE by A2, A7, A9, A11, A13, Th11; :: thesis: verum

end;

then <*p,(PP_composition (f,g)),r*> in SFHTs D ;
hence <*p,(PP_composition (f,g)),r*> is SFHT of D ; :: thesis: verum