let a, b be Real; :: thesis: for t being BinOp of [.0,1.] holds t . (a,b) in [.0,1.]
let t be BinOp of [.0,1.]; :: thesis: t . (a,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: t . (a,b) in [.0,1.]
then [a,b] in [:[.0,1.],[.0,1.]:] by ZFMISC_1:87;
hence t . (a,b) in [.0,1.] by FUNCT_2:5; :: thesis: verum
end;
suppose ( not a in [.0,1.] or not b in [.0,1.] ) ; :: thesis: t . (a,b) in [.0,1.]
then not [a,b] in dom t by ZFMISC_1:87;
then t . [a,b] = 0 by FUNCT_1:def 2;
hence t . (a,b) in [.0,1.] by XXREAL_1:1; :: thesis: verum
end;
end;