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.]

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

suppose ( a in [.0,1.] & b in [.0,1.] ) ; :: thesis: 1 - (f . ((1 - a),(1 - b))) in [.0,1.]

then reconsider aa = a, bb = b as Element of [.0,1.] ;
f . ((1 - aa),(1 - bb)) in [.0,1.] by NormIn01;
hence 1 - (f . ((1 - a),(1 - b))) in [.0,1.] by OpIn01; :: thesis: verum

end;

suppose ( not a in [.0,1.] or not b in [.0,1.] ) ; :: thesis: 1 - (f . ((1 - a),(1 - b))) in [.0,1.]

f . ((1 - a),(1 - b)) in [.0,1.] by NormIn01;
hence 1 - (f . ((1 - a),(1 - b))) in [.0,1.] by OpIn01; :: thesis: verum

end;

end;