Metamath Proof Explorer


Theorem reldmdsmm

Description: The direct sum is a well-behaved binary operator. (Contributed by Stefan O'Rear, 7-Jan-2015)

Ref Expression
Assertion reldmdsmm Reldomm

Proof

Step Hyp Ref Expression
1 df-dsmm m=sV,rVs𝑠r𝑠fxdomrBaserx|xdomr|fx0rxFin
2 1 reldmmpo Reldomm