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

proof

let d be Element of D; :: thesis: ( d in dom p & p . d = TRUE & d in dom (PP_IF (r,f,g)) & (PP_IF (r,f,g)) . d in dom q implies q . ((PP_IF (r,f,g)) . d) = TRUE )
assume that
A3: d in dom p and
A4: p . d = TRUE and
A5: d in dom (PP_IF (r,f,g)) and
A6: (PP_IF (r,f,g)) . d in dom q ; :: thesis: q . ((PP_IF (r,f,g)) . d) = TRUE
A7: dom (PP_and (r,p)) = { d where d is Element of D : ( ( d in dom r & r . d = FALSE ) or ( d in dom p & p . d = FALSE ) or ( d in dom r & r . d = TRUE & d in dom p & p . d = TRUE ) ) } by PARTPR_1:16;
A8: dom (PP_and ((PP_not r),p)) = { d where d is Element of D : ( ( d in dom (PP_not r) & (PP_not r) . d = FALSE ) or ( d in dom p & p . d = FALSE ) or ( d in dom (PP_not r) & (PP_not r) . d = TRUE & d in dom p & p . d = TRUE ) ) } by PARTPR_1:16;
dom (PP_IF (r,f,g)) = { d where d is Element of D : ( ( d in dom r & r . d = TRUE & d in dom f ) or ( d in dom r & r . d = FALSE & d in dom g ) ) } by PARTPR_2:def 11;
then consider d1 being Element of D such that
A9: d = d1 and
A10: ( ( d1 in dom r & r . d1 = TRUE & d1 in dom f ) or ( d1 in dom r & r . d1 = FALSE & d1 in dom g ) ) by A5;
reconsider d1 = d1 as Element of D ;

now :: thesis: q . ((PP_IF (r,f,g)) . d) = TRUE

per cases ( ( d1 in dom r & r . d1 = TRUE & d1 in dom f ) or ( d1 in dom r & r . d1 = FALSE & d1 in dom g ) ) by A10;

suppose that A11: d1 in dom r and
A12: r . d1 = TRUE and
A13: d1 in dom f ; :: thesis: q . ((PP_IF (r,f,g)) . d) = TRUE

A14: (PP_IF (r,f,g)) . d = f . d by A9, A11, A12, A13, PARTPR_2:def 11;
A15: d in dom (PP_and (r,p)) by A3, A4, A7, A9, A11, A12;
(PP_and (r,p)) . d = TRUE by A3, A4, A9, A11, A12, PARTPR_1:18;
hence q . ((PP_IF (r,f,g)) . d) = TRUE by A1, A6, A9, A13, A14, A15, Th11; :: thesis: verum

end;

suppose that A16: d1 in dom r and
A17: r . d1 = FALSE and
A18: d1 in dom g ; :: thesis: q . ((PP_IF (r,f,g)) . d) = TRUE

A19: (PP_IF (r,f,g)) . d = g . d by A9, A16, A17, A18, PARTPR_2:def 11;
A20: d in dom (PP_not r) by A9, A16, PARTPR_1:def 2;
A21: (PP_not r) . d = TRUE by A9, A16, A17, PARTPR_1:def 2;
then A22: (PP_and ((PP_not r),p)) . d = TRUE by A3, A4, A20, PARTPR_1:18;
d in dom (PP_and ((PP_not r),p)) by A3, A4, A8, A20, A21;
hence q . ((PP_IF (r,f,g)) . d) = TRUE by A2, A6, A9, A18, A19, A22, Th11; :: thesis: verum

end;

end;

end;

hence q . ((PP_IF (r,f,g)) . d) = TRUE ; :: thesis: verum

end;

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