Theorem reldmdsmm

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

	Ref	Expression
Assertion	reldmdsmm	|- Rel dom (+)m

Proof

Step	Hyp	Ref	Expression
1		df-dsmm	|- (+)m = ( s e. _V , r e. _V |-> ( ( s Xs_ r ) |`s { f e. X_ x e. dom r ( Base ` ( r ` x ) ) | { x e. dom r | ( f ` x ) =/= ( 0g ` ( r ` x ) ) } e. Fin } ) )
2	1	reldmmpo	|- Rel dom (+)m