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