let D be non empty set ; 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; 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; ( <*(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
; <*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;
( 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
;
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 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
;
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;
verum end; suppose that A16:
d1 in dom r
and A17:
r . d1 = FALSE
and A18:
d1 in dom g
;
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;
verum end;
hence
q . ((PP_IF (r,f,g)) . d) = TRUE
;
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
; verum