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