per cases ( [:TM1,TM2:] is empty or not [:TM1,TM2:] is empty ) ;

suppose [:TM1,TM2:] is empty ; :: thesis: [:TM1,TM2:] is metrizable

hence [:TM1,TM2:] is metrizable ; :: thesis: verum

end;

suppose A1: not [:TM1,TM2:] is empty ; :: thesis: [:TM1,TM2:] is metrizable

then A2: not TM2 is empty ;
consider metr2 being Function of [: the carrier of TM2, the carrier of TM2:],REAL such that
A3: metr2 is_metric_of the carrier of TM2 and
A4: Family_open_set (SpaceMetr ( the carrier of TM2,metr2)) = the topology of TM2 by PCOMPS_1:def 8;
set tm2 = SpaceMetr ( the carrier of TM2,metr2);
consider metr1 being Function of [: the carrier of TM1, the carrier of TM1:],REAL such that
A5: metr1 is_metric_of the carrier of TM1 and
A6: Family_open_set (SpaceMetr ( the carrier of TM1,metr1)) = the topology of TM1 by PCOMPS_1:def 8;
set tm1 = SpaceMetr ( the carrier of TM1,metr1);
A7: not TM1 is empty by A1;
then reconsider tm1 = SpaceMetr ( the carrier of TM1,metr1), tm2 = SpaceMetr ( the carrier of TM2,metr2) as non empty MetrStruct by A5, A3, A2, PCOMPS_1:36;
A8: TopStruct(# the carrier of TM2, the topology of TM2 #) = TopStruct(# the carrier of (TopSpaceMetr tm2), the topology of (TopSpaceMetr tm2) #) by A3, A4, A2, PCOMPS_2:4;
TopStruct(# the carrier of TM1, the topology of TM1 #) = TopStruct(# the carrier of (TopSpaceMetr tm1), the topology of (TopSpaceMetr tm1) #) by A7, A5, A6, PCOMPS_2:4;
then [:TM1,TM2:] = [:(TopSpaceMetr tm1),(TopSpaceMetr tm2):] by A8, WAYBEL29:7
.= TopSpaceMetr (max-Prod2 (tm1,tm2)) by TOPREAL7:23 ;
hence [:TM1,TM2:] is metrizable ; :: thesis: verum

end;

end;