let D be non empty set ; 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; 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; ( <*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
; <*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;
( 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
;
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;
verum
end;
then
<*p,(PP_composition (f,g)),r*> in SFHTs D
;
hence
<*p,(PP_composition (f,g)),r*> is SFHT of D
; verum