defpred S_{3}[ object , object , object , object ] means for p, q being PartialPredicate of D

for f being BinominativeFunction of D st p = $1 & f = $2 & q = $3 holds

for h being Function st h = $4 holds

( dom h = H_{1}(p,f,q) & ( for d being object holds

( ( S_{1}[d,p,f,q] implies h . d = TRUE ) & ( S_{2}[d,p,f,q] implies h . d = FALSE ) ) ) );

A1: for x1 being Element of Pr D

for x2 being Element of FPrg D

for x3 being Element of Pr D ex y being Element of Pr D st S_{3}[x1,x2,x3,y]

A14: for x being Element of Pr D

for y being Element of FPrg D

for z being Element of Pr D holds S_{3}[x,y,z,F . [x,y,z]]
from MULTOP_1:sch 1(A1);

take F ; :: thesis: for p, q being PartialPredicate of D

for f being BinominativeFunction of D holds

( dom (F . (p,f,q)) = { d where d is Element of D : ( ( d in dom p & p . d = FALSE ) or ( d in dom (q * f) & (q * f) . d = TRUE ) or ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE ) ) } & ( for d being object holds

( ( ( ( d in dom p & p . d = FALSE ) or ( d in dom (q * f) & (q * f) . d = TRUE ) ) implies (F . (p,f,q)) . d = TRUE ) & ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE implies (F . (p,f,q)) . d = FALSE ) ) ) )

let p, q be PartialPredicate of D; :: thesis: for f being BinominativeFunction of D holds

( dom (F . (p,f,q)) = { d where d is Element of D : ( ( d in dom p & p . d = FALSE ) or ( d in dom (q * f) & (q * f) . d = TRUE ) or ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE ) ) } & ( for d being object holds

( ( ( ( d in dom p & p . d = FALSE ) or ( d in dom (q * f) & (q * f) . d = TRUE ) ) implies (F . (p,f,q)) . d = TRUE ) & ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE implies (F . (p,f,q)) . d = FALSE ) ) ) )

let f be BinominativeFunction of D; :: thesis: ( dom (F . (p,f,q)) = { d where d is Element of D : ( ( d in dom p & p . d = FALSE ) or ( d in dom (q * f) & (q * f) . d = TRUE ) or ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE ) ) } & ( for d being object holds

( ( ( ( d in dom p & p . d = FALSE ) or ( d in dom (q * f) & (q * f) . d = TRUE ) ) implies (F . (p,f,q)) . d = TRUE ) & ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE implies (F . (p,f,q)) . d = FALSE ) ) ) )

( p in Pr D & f in FPrg D & q in Pr D ) by PARTFUN1:45;

hence ( dom (F . (p,f,q)) = { d where d is Element of D : ( ( d in dom p & p . d = FALSE ) or ( d in dom (q * f) & (q * f) . d = TRUE ) or ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE ) ) } & ( for d being object holds

( ( ( ( d in dom p & p . d = FALSE ) or ( d in dom (q * f) & (q * f) . d = TRUE ) ) implies (F . (p,f,q)) . d = TRUE ) & ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE implies (F . (p,f,q)) . d = FALSE ) ) ) ) by A14; :: thesis: verum

for f being BinominativeFunction of D st p = $1 & f = $2 & q = $3 holds

for h being Function st h = $4 holds

( dom h = H

( ( S

A1: for x1 being Element of Pr D

for x2 being Element of FPrg D

for x3 being Element of Pr D ex y being Element of Pr D st S

proof

consider F being Function of [:(Pr D),(FPrg D),(Pr D):],(Pr D) such that
let x1 be Element of Pr D; :: thesis: for x2 being Element of FPrg D

for x3 being Element of Pr D ex y being Element of Pr D st S_{3}[x1,x2,x3,y]

let x2 be Element of FPrg D; :: thesis: for x3 being Element of Pr D ex y being Element of Pr D st S_{3}[x1,x2,x3,y]

let x3 be Element of Pr D; :: thesis: ex y being Element of Pr D st S_{3}[x1,x2,x3,y]

reconsider X1 = x1, X3 = x3 as PartFunc of D,BOOLEAN by PARTFUN1:46;

reconsider X2 = x2 as PartFunc of D,D by PARTFUN1:46;

defpred S_{4}[ object , object ] means for d being object st d = $1 holds

( ( S_{1}[d,X1,X2,X3] implies $2 = TRUE ) & ( S_{2}[d,X1,X2,X3] implies $2 = FALSE ) );

A2: for a being object st a in H_{1}(X1,X2,X3) holds

ex b being object st

( b in BOOLEAN & S_{4}[a,b] )

A7: dom g = H_{1}(X1,X2,X3)
and

A8: rng g c= BOOLEAN and

A9: for x being object st x in H_{1}(X1,X2,X3) holds

S_{4}[x,g . x]
from FUNCT_1:sch 6(A2);

H_{1}(X1,X2,X3) c= D

then reconsider g = g as Element of Pr D by PARTFUN1:45;

take g ; :: thesis: S_{3}[x1,x2,x3,g]

let p, q be PartialPredicate of D; :: thesis: for f being BinominativeFunction of D st p = x1 & f = x2 & q = x3 holds

for h being Function st h = g holds

( dom h = H_{1}(p,f,q) & ( for d being object holds

( ( S_{1}[d,p,f,q] implies h . d = TRUE ) & ( S_{2}[d,p,f,q] implies h . d = FALSE ) ) ) )

let f be BinominativeFunction of D; :: thesis: ( p = x1 & f = x2 & q = x3 implies for h being Function st h = g holds

( dom h = H_{1}(p,f,q) & ( for d being object holds

( ( S_{1}[d,p,f,q] implies h . d = TRUE ) & ( S_{2}[d,p,f,q] implies h . d = FALSE ) ) ) ) )

assume A10: ( x1 = p & x2 = f & x3 = q ) ; :: thesis: for h being Function st h = g holds

( dom h = H_{1}(p,f,q) & ( for d being object holds

( ( S_{1}[d,p,f,q] implies h . d = TRUE ) & ( S_{2}[d,p,f,q] implies h . d = FALSE ) ) ) )

let h be Function; :: thesis: ( h = g implies ( dom h = H_{1}(p,f,q) & ( for d being object holds

( ( S_{1}[d,p,f,q] implies h . d = TRUE ) & ( S_{2}[d,p,f,q] implies h . d = FALSE ) ) ) ) )

assume A11: h = g ; :: thesis: ( dom h = H_{1}(p,f,q) & ( for d being object holds

( ( S_{1}[d,p,f,q] implies h . d = TRUE ) & ( S_{2}[d,p,f,q] implies h . d = FALSE ) ) ) )

thus dom h = H_{1}(p,f,q)
by A7, A10, A11; :: thesis: for d being object holds

( ( S_{1}[d,p,f,q] implies h . d = TRUE ) & ( S_{2}[d,p,f,q] implies h . d = FALSE ) )

let d be object ; :: thesis: ( ( S_{1}[d,p,f,q] implies h . d = TRUE ) & ( S_{2}[d,p,f,q] implies h . d = FALSE ) )

_{2}[d,p,f,q]
; :: thesis: h . d = FALSE

then d in dom p ;

then d in H_{1}(X1,X2,X3)
by A10, A13;

hence h . d = FALSE by A9, A10, A11, A13; :: thesis: verum

end;for x3 being Element of Pr D ex y being Element of Pr D st S

let x2 be Element of FPrg D; :: thesis: for x3 being Element of Pr D ex y being Element of Pr D st S

let x3 be Element of Pr D; :: thesis: ex y being Element of Pr D st S

reconsider X1 = x1, X3 = x3 as PartFunc of D,BOOLEAN by PARTFUN1:46;

reconsider X2 = x2 as PartFunc of D,D by PARTFUN1:46;

defpred S

( ( S

A2: for a being object st a in H

ex b being object st

( b in BOOLEAN & S

proof

consider g being Function such that
let a be object ; :: thesis: ( a in H_{1}(X1,X2,X3) implies ex b being object st

( b in BOOLEAN & S_{4}[a,b] ) )

assume a in H_{1}(X1,X2,X3)
; :: thesis: ex b being object st

( b in BOOLEAN & S_{4}[a,b] )

then consider d being Element of D such that

A3: d = a and

A4: ( S_{1}[d,X1,X2,X3] or S_{2}[d,X1,X2,X3] )
;

end;( b in BOOLEAN & S

assume a in H

( b in BOOLEAN & S

then consider d being Element of D such that

A3: d = a and

A4: ( S

per cases
( S_{1}[d,X1,X2,X3] or S_{2}[d,X1,X2,X3] )
by A4;

end;

suppose A5:
S_{1}[d,X1,X2,X3]
; :: thesis: ex b being object st

( b in BOOLEAN & S_{4}[a,b] )

( b in BOOLEAN & S

take
TRUE
; :: thesis: ( TRUE in BOOLEAN & S_{4}[a, TRUE ] )

thus ( TRUE in BOOLEAN & S_{4}[a, TRUE ] )
by A3, A5; :: thesis: verum

end;thus ( TRUE in BOOLEAN & S

suppose A6:
S_{2}[d,X1,X2,X3]
; :: thesis: ex b being object st

( b in BOOLEAN & S_{4}[a,b] )

( b in BOOLEAN & S

take
FALSE
; :: thesis: ( FALSE in BOOLEAN & S_{4}[a, FALSE ] )

thus ( FALSE in BOOLEAN & S_{4}[a, FALSE ] )
by A3, A6; :: thesis: verum

end;thus ( FALSE in BOOLEAN & S

A7: dom g = H

A8: rng g c= BOOLEAN and

A9: for x being object st x in H

S

H

proof

then
g is PartFunc of D,BOOLEAN
by A7, A8, RELSET_1:4;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H_{1}(X1,X2,X3) or x in D )

assume x in H_{1}(X1,X2,X3)
; :: thesis: x in D

then ex d being Element of D st

( d = x & ( S_{1}[d,X1,X2,X3] or S_{2}[d,X1,X2,X3] ) )
;

hence x in D ; :: thesis: verum

end;assume x in H

then ex d being Element of D st

( d = x & ( S

hence x in D ; :: thesis: verum

then reconsider g = g as Element of Pr D by PARTFUN1:45;

take g ; :: thesis: S

let p, q be PartialPredicate of D; :: thesis: for f being BinominativeFunction of D st p = x1 & f = x2 & q = x3 holds

for h being Function st h = g holds

( dom h = H

( ( S

let f be BinominativeFunction of D; :: thesis: ( p = x1 & f = x2 & q = x3 implies for h being Function st h = g holds

( dom h = H

( ( S

assume A10: ( x1 = p & x2 = f & x3 = q ) ; :: thesis: for h being Function st h = g holds

( dom h = H

( ( S

let h be Function; :: thesis: ( h = g implies ( dom h = H

( ( S

assume A11: h = g ; :: thesis: ( dom h = H

( ( S

thus dom h = H

( ( S

let d be object ; :: thesis: ( ( S

hereby :: thesis: ( S_{2}[d,p,f,q] implies h . d = FALSE )

assume A13:
Sassume A12:
S_{1}[d,p,f,q]
; :: thesis: h . d = TRUE

then ( d in dom p or d in dom (q * f) ) ;

then d in H_{1}(X1,X2,X3)
by A10, A12;

hence h . d = TRUE by A9, A10, A11, A12; :: thesis: verum

end;then ( d in dom p or d in dom (q * f) ) ;

then d in H

hence h . d = TRUE by A9, A10, A11, A12; :: thesis: verum

then d in dom p ;

then d in H

hence h . d = FALSE by A9, A10, A11, A13; :: thesis: verum

A14: for x being Element of Pr D

for y being Element of FPrg D

for z being Element of Pr D holds S

take F ; :: thesis: for p, q being PartialPredicate of D

for f being BinominativeFunction of D holds

( dom (F . (p,f,q)) = { d where d is Element of D : ( ( d in dom p & p . d = FALSE ) or ( d in dom (q * f) & (q * f) . d = TRUE ) or ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE ) ) } & ( for d being object holds

( ( ( ( d in dom p & p . d = FALSE ) or ( d in dom (q * f) & (q * f) . d = TRUE ) ) implies (F . (p,f,q)) . d = TRUE ) & ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE implies (F . (p,f,q)) . d = FALSE ) ) ) )

let p, q be PartialPredicate of D; :: thesis: for f being BinominativeFunction of D holds

( dom (F . (p,f,q)) = { d where d is Element of D : ( ( d in dom p & p . d = FALSE ) or ( d in dom (q * f) & (q * f) . d = TRUE ) or ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE ) ) } & ( for d being object holds

( ( ( ( d in dom p & p . d = FALSE ) or ( d in dom (q * f) & (q * f) . d = TRUE ) ) implies (F . (p,f,q)) . d = TRUE ) & ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE implies (F . (p,f,q)) . d = FALSE ) ) ) )

let f be BinominativeFunction of D; :: thesis: ( dom (F . (p,f,q)) = { d where d is Element of D : ( ( d in dom p & p . d = FALSE ) or ( d in dom (q * f) & (q * f) . d = TRUE ) or ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE ) ) } & ( for d being object holds

( ( ( ( d in dom p & p . d = FALSE ) or ( d in dom (q * f) & (q * f) . d = TRUE ) ) implies (F . (p,f,q)) . d = TRUE ) & ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE implies (F . (p,f,q)) . d = FALSE ) ) ) )

( p in Pr D & f in FPrg D & q in Pr D ) by PARTFUN1:45;

hence ( dom (F . (p,f,q)) = { d where d is Element of D : ( ( d in dom p & p . d = FALSE ) or ( d in dom (q * f) & (q * f) . d = TRUE ) or ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE ) ) } & ( for d being object holds

( ( ( ( d in dom p & p . d = FALSE ) or ( d in dom (q * f) & (q * f) . d = TRUE ) ) implies (F . (p,f,q)) . d = TRUE ) & ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE implies (F . (p,f,q)) . d = FALSE ) ) ) ) by A14; :: thesis: verum