let D be non empty set ; :: thesis: for f, g being BinominativeFunction of D
for p, q, r, s being PartialPredicate of D st <*p,f,q*> is SFHT of D & <*q,g,r*> is SFHT of D & <*(PP_inversion q),g,s*> is SFHT of D holds
<*p,(PP_composition (f,g)),(PP_or (r,s))*> is SFHT of D
let f, g be BinominativeFunction of D; :: thesis: for p, q, r, s being PartialPredicate of D st <*p,f,q*> is SFHT of D & <*q,g,r*> is SFHT of D & <*(PP_inversion q),g,s*> is SFHT of D holds
<*p,(PP_composition (f,g)),(PP_or (r,s))*> is SFHT of D
let p, q, r, s be PartialPredicate of D; :: thesis: ( <*p,f,q*> is SFHT of D & <*q,g,r*> is SFHT of D & <*(PP_inversion q),g,s*> is SFHT of D implies <*p,(PP_composition (f,g)),(PP_or (r,s))*> 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: <*(PP_inversion q),g,s*> is SFHT of D ; :: thesis: <*p,(PP_composition (f,g)),(PP_or (r,s))*> 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 (PP_or (r,s)) holds
(PP_or (r,s)) . ((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 (PP_or (r,s)) implies (PP_or (r,s)) . ((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 (PP_or (r,s)) ; :: thesis: (PP_or (r,s)) . ((PP_composition (f,g)) . d) = TRUE
set d1 = f . d;
assume (PP_or (r,s)) . ((PP_composition (f,g)) . d) <> TRUE ; :: thesis: contradiction
then A8: (PP_or (r,s)) . ((PP_composition (f,g)) . d) = FALSE by A7, PARTPR_1:3;
then A9: ( (PP_composition (f,g)) . d in dom r & r . ((PP_composition (f,g)) . d) = FALSE ) by A7, PARTPR_1:13;
A10: ( (PP_composition (f,g)) . d in dom s & s . ((PP_composition (f,g)) . d) = FALSE ) by A7, A8, PARTPR_1:13;
A11: PP_composition (f,g) = g * f by PARTPR_2:def 1;
then A12: (PP_composition (f,g)) . d = g . (f . d) by A6, FUNCT_1:12;
A13: d in dom f by A6, A11, FUNCT_1:11;
then A14: f . d in D by PARTFUN1:4;
A15: f . d in dom g by A6, A11, FUNCT_1:11;

per cases ( f . d in dom q or not f . d in dom q ) ;

suppose A16: f . d in dom q ; :: thesis: contradiction

then q . (f . d) = TRUE by A1, A4, A5, A13, Th11;
hence contradiction by A2, A9, A12, A16, A15, Th11; :: thesis: verum

end;

suppose A17: not f . d in dom q ; :: thesis: contradiction

set I = PP_inversion q;
A18: (PP_inversion q) . (f . d) = TRUE by A14, A17, PARTPR_2:def 17;
dom (PP_inversion q) = { d where d is Element of D : not d in dom q } by PARTPR_2:def 17;
then f . d in dom (PP_inversion q) by A17, A14;
hence contradiction by A3, A15, A10, A12, A18, Th11; :: thesis: verum

end;

end;

end;

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