A1: rng T1 c= D1 by RELAT_1:def 19;
A2: rng T2 c= D2 by RELAT_1:def 19;
A3: rng <:T1,T2:> c= [:(rng T1),(rng T2):] by FUNCT_3:51;
[:(rng T1),(rng T2):] c= [:D1,D2:] by A1, A2, ZFMISC_1:96;
then rng <:T1,T2:> c= [:D1,D2:] by A3, XBOOLE_1:1;
hence <:T1,T2:> is [:D1,D2:] -valued by RELAT_1:def 19; :: thesis: verum