let f be BinOp of [.0,1.]; :: thesis: for a, b being Real holds 1 - (f . ((1 - a),(1 - b))) in [.0,1.]

let a, b be Real; :: thesis: 1 - (f . ((1 - a),(1 - b))) in [.0,1.]

let a, b be Real; :: thesis: 1 - (f . ((1 - a),(1 - b))) in [.0,1.]

per cases
( ( a in [.0,1.] & b in [.0,1.] ) or not a in [.0,1.] or not b in [.0,1.] )
;

end;