defpred S1[ object , object , object ] means ( ( P1[$1,$2] & $3 = TRUE ) or ( P1[$1,$2] & $3 = FALSE ) );
A1: for x, y being object st x in F1() & y in F2() holds
ex z being object st
( z in BOOLEAN & S1[x,y,z] )
proof
let x, y be object ; :: thesis: ( x in F1() & y in F2() implies ex z being object st
( z in BOOLEAN & S1[x,y,z] ) )
assume ( x in F1() & y in F2() ) ; :: thesis: ex z being object st
( z in BOOLEAN & S1[x,y,z] )
per cases ( S1[x,y, TRUE ] or S1[x,y, FALSE ] ) ;
suppose A2: S1[x,y, TRUE ] ; :: thesis: ex z being object st
( z in BOOLEAN & S1[x,y,z] )
take TRUE ; :: thesis: ( TRUE in BOOLEAN & S1[x,y, TRUE ] )
thus ( TRUE in BOOLEAN & S1[x,y, TRUE ] ) by A2; :: thesis: verum
end;
suppose A3: S1[x,y, FALSE ] ; :: thesis: ex z being object st
( z in BOOLEAN & S1[x,y,z] )
take FALSE ; :: thesis: ( FALSE in BOOLEAN & S1[x,y, FALSE ] )
thus ( FALSE in BOOLEAN & S1[x,y, FALSE ] ) by A3; :: thesis: verum
end;
end;
end;
consider f being Function of [:F1(),F2():],BOOLEAN such that
A4: for x, y being object st x in F1() & y in F2() holds
S1[x,y,f . (x,y)] from BINOP_1:sch 1(A1);
 take f ; :: thesis: for x, y being object st x in F1() & y in F2() holds
( ( P1[x,y] implies f . (x,y) = TRUE ) & ( P1[x,y] implies f . (x,y) = FALSE ) )
thus for x, y being object st x in F1() & y in F2() holds
( ( P1[x,y] implies f . (x,y) = TRUE ) & ( P1[x,y] implies f . (x,y) = FALSE ) ) by A4; :: thesis: verum