Theorem ofmresval

Description: Value of a restriction of the function operation map. (Contributed by NM, 20-Oct-2014)

	Ref	Expression
Hypotheses	ofmresval.f	|- ( ph -> F e. A )
	ofmresval.g	|- ( ph -> G e. B )
Assertion	ofmresval	|- ( ph -> ( F ( oF R |` ( A X. B ) ) G ) = ( F oF R G ) )

Proof

Step	Hyp	Ref	Expression
1		ofmresval.f	|- ( ph -> F e. A )
2		ofmresval.g	|- ( ph -> G e. B )
3		ovres	|- ( ( F e. A /\ G e. B ) -> ( F ( oF R |` ( A X. B ) ) G ) = ( F oF R G ) )
4	1 2 3	syl2anc	|- ( ph -> ( F ( oF R |` ( A X. B ) ) G ) = ( F oF R G ) )