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 TM1 is empty ;
consider metr1 being Function of [:the carrier of TM1,the carrier of TM1:],REAL such that
A3: metr1 is_metric_of the carrier of TM1 and
A4: Family_open_set (SpaceMetr the carrier of TM1,metr1) = the topology of TM1 by PCOMPS_1:def 9;
set tm1 = SpaceMetr the carrier of TM1,metr1;
consider metr2 being Function of [:the carrier of TM2,the carrier of TM2:],REAL such that
A5: metr2 is_metric_of the carrier of TM2 and
A6: Family_open_set (SpaceMetr the carrier of TM2,metr2) = the topology of TM2 by PCOMPS_1:def 9;
set tm2 = SpaceMetr the carrier of TM2,metr2;
A7: not TM2 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:40;
A8: TopStruct(# the carrier of TM1,the topology of TM1 #) = TopStruct(# the carrier of (TopSpaceMetr tm1),the topology of (TopSpaceMetr tm1) #) by A3, A4, A2, PCOMPS_2:8;
TopStruct(# the carrier of TM2,the topology of TM2 #) = TopStruct(# the carrier of (TopSpaceMetr tm2),the topology of (TopSpaceMetr tm2) #) by A7, A5, A6, PCOMPS_2:8;
then [:TM1,TM2:] = [:(TopSpaceMetr tm1),(TopSpaceMetr tm2):] by A8, WAYBEL29:10
.= TopSpaceMetr (max-Prod2 tm1,tm2) by TOPREAL7:25 ;
hence [:TM1,TM2:] is metrizable ; :: thesis: verum

end;

end;