defpred S₁[ object , object , object ] means ( ( P₁[$1,$2] & $3 = TRUE ) or ( P₁[$1,$2] & $3 = FALSE ) );
A1: for x, y being object st x in F₁() & y in F₂() holds
ex z being object st
( z in BOOLEAN & S₁[x,y,z] )

proof

let x, y be object ; :: thesis: ( x in F₁() & y in F₂() implies ex z being object st
( z in BOOLEAN & S₁[x,y,z] ) )
assume ( x in F₁() & y in F₂() ) ; :: thesis: ex z being object st
( z in BOOLEAN & S₁[x,y,z] )

per cases ( S₁[x,y, TRUE ] or S₁[x,y, FALSE ] ) ;

suppose A2: S₁[x,y, TRUE ] ; :: thesis: ex z being object st
( z in BOOLEAN & S₁[x,y,z] )

take TRUE ; :: thesis: ( TRUE in BOOLEAN & S₁[x,y, TRUE ] )
thus ( TRUE in BOOLEAN & S₁[x,y, TRUE ] ) by A2; :: thesis: verum

end;

suppose A3: S₁[x,y, FALSE ] ; :: thesis: ex z being object st
( z in BOOLEAN & S₁[x,y,z] )

take FALSE ; :: thesis: ( FALSE in BOOLEAN & S₁[x,y, FALSE ] )
thus ( FALSE in BOOLEAN & S₁[x,y, FALSE ] ) by A3; :: thesis: verum

end;

end;

end;

consider f being Function of [:F₁(),F₂():],BOOLEAN such that
A4: for x, y being object st x in F₁() & y in F₂() holds
S₁[x,y,f . (x,y)] from BINOP_1:sch 1(A1);
take f ; :: thesis: for x, y being object st x in F₁() & y in F₂() holds
( ( P₁[x,y] implies f . (x,y) = TRUE ) & ( P₁[x,y] implies f . (x,y) = FALSE ) )
thus for x, y being object st x in F₁() & y in F₂() holds
( ( P₁[x,y] implies f . (x,y) = TRUE ) & ( P₁[x,y] implies f . (x,y) = FALSE ) ) by A4; :: thesis: verum