defpred S3[ object , object , object ] means for p, q being PartialPredicate of D st $1 = p & $2 = q holds
for f being Function st f = $3 holds
( dom f = H1(p,q) & ( for d being object holds
( ( ( S1[d,p] or S1[d,q] ) implies f . d = TRUE ) & ( S2[d,p,q] implies f . d = FALSE ) ) ) );
A1: for x1, x2 being object st x1 in Pr D & x2 in Pr D holds
ex y being object st
( y in Pr D & S3[x1,x2,y] )
proof
let x1, x2 be object ; :: thesis: ( x1 in Pr D & x2 in Pr D implies ex y being object st
( y in Pr D & S3[x1,x2,y] ) )
assume ( x1 in Pr D & x2 in Pr D ) ; :: thesis: ex y being object st
( y in Pr D & S3[x1,x2,y] )
then reconsider X1 = x1, X2 = x2 as PartFunc of D,BOOLEAN by PARTFUN1:46;
defpred S4[ object , object ] means for d being Element of D st d = $1 holds
( ( ( S1[d,X1] or S1[d,X2] ) implies $2 = TRUE ) & ( S2[d,X1,X2] implies $2 = FALSE ) );
A2: for a being object st a in H1(X1,X2) holds
ex b being object st
( b in BOOLEAN & S4[a,b] )
proof
let a be object ; :: thesis: ( a in H1(X1,X2) implies ex b being object st
( b in BOOLEAN & S4[a,b] ) )
assume a in H1(X1,X2) ; :: thesis: ex b being object st
( b in BOOLEAN & S4[a,b] )
then consider d being Element of D such that
A3: d = a and
A4: ( S1[d,X1] or S1[d,X2] or S2[d,X1,X2] ) ;
end;
consider g being Function such that
A7: dom g = H1(X1,X2) and
A8: rng g c= BOOLEAN and
A9: for x being object st x in H1(X1,X2) holds
S4[x,g . x] from FUNCT_1:sch 6(A2);
 take g ; :: thesis: ( g in Pr D & S3[x1,x2,g] )
H1(X1,X2) c= D
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H1(X1,X2) or x in D )
assume x in H1(X1,X2) ; :: thesis: x in D
then ex d being Element of D st
( d = x & ( S1[d,X1] or S1[d,X2] or S2[d,X1,X2] ) ) ;
hence x in D ; :: thesis: verum
end;
then g is PartFunc of D,BOOLEAN by A7, A8, RELSET_1:4;
hence g in Pr D by PARTFUN1:45; :: thesis: S3[x1,x2,g]
let p, q be PartialPredicate of D; :: thesis: ( x1 = p & x2 = q implies for f being Function st f = g holds
( dom f = H1(p,q) & ( for d being object holds
( ( ( S1[d,p] or S1[d,q] ) implies f . d = TRUE ) & ( S2[d,p,q] implies f . d = FALSE ) ) ) ) )
assume A10: ( x1 = p & x2 = q ) ; :: thesis: for f being Function st f = g holds
( dom f = H1(p,q) & ( for d being object holds
( ( ( S1[d,p] or S1[d,q] ) implies f . d = TRUE ) & ( S2[d,p,q] implies f . d = FALSE ) ) ) )
let f be Function; :: thesis: ( f = g implies ( dom f = H1(p,q) & ( for d being object holds
( ( ( S1[d,p] or S1[d,q] ) implies f . d = TRUE ) & ( S2[d,p,q] implies f . d = FALSE ) ) ) ) )
assume A11: f = g ; :: thesis: ( dom f = H1(p,q) & ( for d being object holds
( ( ( S1[d,p] or S1[d,q] ) implies f . d = TRUE ) & ( S2[d,p,q] implies f . d = FALSE ) ) ) )
thus dom f = H1(p,q) by A7, A10, A11; :: thesis: for d being object holds
( ( ( S1[d,p] or S1[d,q] ) implies f . d = TRUE ) & ( S2[d,p,q] implies f . d = FALSE ) )
let d be object ; :: thesis: ( ( ( S1[d,p] or S1[d,q] ) implies f . d = TRUE ) & ( S2[d,p,q] implies f . d = FALSE ) )
hereby :: thesis: ( S2[d,p,q] implies f . d = FALSE )
assume A12: ( S1[d,p] or S1[d,q] ) ; :: thesis: f . d = TRUE
then ( d in dom p or d in dom q ) ;
then A13: d is Element of D ;
then d in H1(X1,X2) by A10, A12;
hence f . d = TRUE by A9, A10, A11, A12, A13; :: thesis: verum
end;
assume A14: S2[d,p,q] ; :: thesis: f . d = FALSE
then d in dom p ;
then A15: d is Element of D ;
then d in H1(X1,X2) by A10, A14;
hence f . d = FALSE by A9, A10, A11, A14, A15; :: thesis: verum
end;
consider F being Function of [:(Pr D),(Pr D):],(Pr D) such that
A16: for x, y being object st x in Pr D & y in Pr D holds
S3[x,y,F . (x,y)] from BINOP_1:sch 1(A1);
 take F ; :: thesis: for p, q being PartialPredicate of D holds
( dom (F . (p,q)) = { d where d is Element of D : ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE ) ) } & ( for d being object holds
( ( ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) ) implies (F . (p,q)) . d = TRUE ) & ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE implies (F . (p,q)) . d = FALSE ) ) ) )
let p, q be PartialPredicate of D; :: thesis: ( dom (F . (p,q)) = { d where d is Element of D : ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE ) ) } & ( for d being object holds
( ( ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) ) implies (F . (p,q)) . d = TRUE ) & ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE implies (F . (p,q)) . d = FALSE ) ) ) )
( p in Pr D & q in Pr D ) by PARTFUN1:45;
hence ( dom (F . (p,q)) = { d where d is Element of D : ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE ) ) } & ( for d being object holds
( ( ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) ) implies (F . (p,q)) . d = TRUE ) & ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE implies (F . (p,q)) . d = FALSE ) ) ) ) by A16; :: thesis: verum