Description: Image of a cartesian product for a function on ordered pairs with values expressed as ordered pairs. Note that F and G are the projections of H to the first and second coordinate respectively. (Contributed by Thierry Arnoux, 30-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | fvproj.h | |
|
fimaproj.f | |
||
fimaproj.g | |
||
fimaproj.x | |
||
fimaproj.y | |
||
Assertion | fimaproj | |