( D2 = {} implies [:D2,D2:] = {} )
by ZFMISC_1:90;

then A1: dom f2 = [:D2,D2:] by FUNCT_2:def 1;

A2: rng f2 c= D2 by RELAT_1:def 19;

rng f1 c= D1 by RELAT_1:def 19;

then A3: [:(rng f1),(rng f2):] c= [:D1,D2:] by A2, ZFMISC_1:96;

A4: rng |:f1,f2:| c= [:(rng f1),(rng f2):] by FUNCT_4:56;

( D1 = {} implies [:D1,D1:] = {} ) by ZFMISC_1:90;

then dom f1 = [:D1,D1:] by FUNCT_2:def 1;

then dom |:f1,f2:| = [:[:D1,D2:],[:D1,D2:]:] by A1, FUNCT_4:58;

hence |:f1,f2:| is BinOp of [:D1,D2:] by A3, A4, FUNCT_2:2, XBOOLE_1:1; :: thesis: verum

then A1: dom f2 = [:D2,D2:] by FUNCT_2:def 1;

A2: rng f2 c= D2 by RELAT_1:def 19;

rng f1 c= D1 by RELAT_1:def 19;

then A3: [:(rng f1),(rng f2):] c= [:D1,D2:] by A2, ZFMISC_1:96;

A4: rng |:f1,f2:| c= [:(rng f1),(rng f2):] by FUNCT_4:56;

( D1 = {} implies [:D1,D1:] = {} ) by ZFMISC_1:90;

then dom f1 = [:D1,D1:] by FUNCT_2:def 1;

then dom |:f1,f2:| = [:[:D1,D2:],[:D1,D2:]:] by A1, FUNCT_4:58;

hence |:f1,f2:| is BinOp of [:D1,D2:] by A3, A4, FUNCT_2:2, XBOOLE_1:1; :: thesis: verum