defpred S₃[ 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₁(p,f,q) & ( for d being object holds
( ( S₁[d,p,f,q] implies h . d = TRUE ) & ( S₂[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₃[x1,x2,x3,y]

proof

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₃[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₃[x1,x2,x3,y]
let x3 be Element of Pr D; :: thesis: ex y being Element of Pr D st S₃[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₄[ object , object ] means for d being object st d = $1 holds
( ( S₁[d,X1,X2,X3] implies $2 = TRUE ) & ( S₂[d,X1,X2,X3] implies $2 = FALSE ) );
A2: for a being object st a in H₁(X1,X2,X3) holds
ex b being object st
( b in BOOLEAN & S₄[a,b] )

proof

let a be object ; :: thesis: ( a in H₁(X1,X2,X3) implies ex b being object st
( b in BOOLEAN & S₄[a,b] ) )
assume a in H₁(X1,X2,X3) ; :: thesis: ex b being object st
( b in BOOLEAN & S₄[a,b] )
then consider d being Element of D such that
A3: d = a and
A4: ( S₁[d,X1,X2,X3] or S₂[d,X1,X2,X3] ) ;

per cases ( S₁[d,X1,X2,X3] or S₂[d,X1,X2,X3] ) by A4;

suppose A5: S₁[d,X1,X2,X3] ; :: thesis: ex b being object st
( b in BOOLEAN & S₄[a,b] )

take TRUE ; :: thesis: ( TRUE in BOOLEAN & S₄[a, TRUE ] )
thus ( TRUE in BOOLEAN & S₄[a, TRUE ] ) by A3, A5; :: thesis: verum

end;

suppose A6: S₂[d,X1,X2,X3] ; :: thesis: ex b being object st
( b in BOOLEAN & S₄[a,b] )

take FALSE ; :: thesis: ( FALSE in BOOLEAN & S₄[a, FALSE ] )
thus ( FALSE in BOOLEAN & S₄[a, FALSE ] ) by A3, A6; :: thesis: verum

end;

end;

end;

consider g being Function such that
A7: dom g = H₁(X1,X2,X3) and
A8: rng g c= BOOLEAN and
A9: for x being object st x in H₁(X1,X2,X3) holds
S₄[x,g . x] from FUNCT_1:sch 6(A2);
H₁(X1,X2,X3) c= D

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H₁(X1,X2,X3) or x in D )
assume x in H₁(X1,X2,X3) ; :: thesis: x in D
then ex d being Element of D st
( d = x & ( S₁[d,X1,X2,X3] or S₂[d,X1,X2,X3] ) ) ;
hence x in D ; :: thesis: verum

end;

then g is PartFunc of D,BOOLEAN by A7, A8, RELSET_1:4;
then reconsider g = g as Element of Pr D by PARTFUN1:45;
take g ; :: thesis: S₃[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₁(p,f,q) & ( for d being object holds
( ( S₁[d,p,f,q] implies h . d = TRUE ) & ( S₂[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₁(p,f,q) & ( for d being object holds
( ( S₁[d,p,f,q] implies h . d = TRUE ) & ( S₂[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₁(p,f,q) & ( for d being object holds
( ( S₁[d,p,f,q] implies h . d = TRUE ) & ( S₂[d,p,f,q] implies h . d = FALSE ) ) ) )
let h be Function; :: thesis: ( h = g implies ( dom h = H₁(p,f,q) & ( for d being object holds
( ( S₁[d,p,f,q] implies h . d = TRUE ) & ( S₂[d,p,f,q] implies h . d = FALSE ) ) ) ) )
assume A11: h = g ; :: thesis: ( dom h = H₁(p,f,q) & ( for d being object holds
( ( S₁[d,p,f,q] implies h . d = TRUE ) & ( S₂[d,p,f,q] implies h . d = FALSE ) ) ) )
thus dom h = H₁(p,f,q) by A7, A10, A11; :: thesis: for d being object holds
( ( S₁[d,p,f,q] implies h . d = TRUE ) & ( S₂[d,p,f,q] implies h . d = FALSE ) )
let d be object ; :: thesis: ( ( S₁[d,p,f,q] implies h . d = TRUE ) & ( S₂[d,p,f,q] implies h . d = FALSE ) )

hereby :: thesis: ( S₂[d,p,f,q] implies h . d = FALSE )

assume A12: S₁[d,p,f,q] ; :: thesis: h . d = TRUE
then ( d in dom p or d in dom (q * f) ) ;
then d in H₁(X1,X2,X3) by A10, A12;
hence h . d = TRUE by A9, A10, A11, A12; :: thesis: verum

end;

assume A13: S₂[d,p,f,q] ; :: thesis: h . d = FALSE
then d in dom p ;
then d in H₁(X1,X2,X3) by A10, A13;
hence h . d = FALSE by A9, A10, A11, A13; :: thesis: verum

end;

consider F being Function of [:(Pr D),(FPrg D),(Pr D):],(Pr D) such that
A14: for x being Element of Pr D
for y being Element of FPrg D
for z being Element of Pr D holds S₃[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