# Metamath Proof Explorer

## Theorem ofco2

Description: Distribution law for the function operation and the composition of functions. (Contributed by Stefan O'Rear, 17-Jul-2018)

Ref Expression
Assertion ofco2 ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹𝐻 ) ∈ V ∧ ( 𝐺𝐻 ) ∈ V ) ) → ( ( 𝐹f 𝑅 𝐺 ) ∘ 𝐻 ) = ( ( 𝐹𝐻 ) ∘f 𝑅 ( 𝐺𝐻 ) ) )

### Proof

Step Hyp Ref Expression
1 simpr1 ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹𝐻 ) ∈ V ∧ ( 𝐺𝐻 ) ∈ V ) ) → Fun 𝐻 )
2 fvimacnvi ( ( Fun 𝐻𝑥 ∈ ( 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( 𝐻𝑥 ) ∈ ( dom 𝐹 ∩ dom 𝐺 ) )
3 1 2 sylan ( ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹𝐻 ) ∈ V ∧ ( 𝐺𝐻 ) ∈ V ) ) ∧ 𝑥 ∈ ( 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( 𝐻𝑥 ) ∈ ( dom 𝐹 ∩ dom 𝐺 ) )
4 1 funfnd ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹𝐻 ) ∈ V ∧ ( 𝐺𝐻 ) ∈ V ) ) → 𝐻 Fn dom 𝐻 )
5 dffn5 ( 𝐻 Fn dom 𝐻𝐻 = ( 𝑥 ∈ dom 𝐻 ↦ ( 𝐻𝑥 ) ) )
6 4 5 sylib ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹𝐻 ) ∈ V ∧ ( 𝐺𝐻 ) ∈ V ) ) → 𝐻 = ( 𝑥 ∈ dom 𝐻 ↦ ( 𝐻𝑥 ) ) )
7 6 reseq1d ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹𝐻 ) ∈ V ∧ ( 𝐺𝐻 ) ∈ V ) ) → ( 𝐻 ↾ ( 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ) = ( ( 𝑥 ∈ dom 𝐻 ↦ ( 𝐻𝑥 ) ) ↾ ( 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ) )
8 cnvimass ( 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ⊆ dom 𝐻
9 resmpt ( ( 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ⊆ dom 𝐻 → ( ( 𝑥 ∈ dom 𝐻 ↦ ( 𝐻𝑥 ) ) ↾ ( 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ) = ( 𝑥 ∈ ( 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ↦ ( 𝐻𝑥 ) ) )
10 8 9 ax-mp ( ( 𝑥 ∈ dom 𝐻 ↦ ( 𝐻𝑥 ) ) ↾ ( 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ) = ( 𝑥 ∈ ( 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ↦ ( 𝐻𝑥 ) )
11 7 10 eqtrdi ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹𝐻 ) ∈ V ∧ ( 𝐺𝐻 ) ∈ V ) ) → ( 𝐻 ↾ ( 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ) = ( 𝑥 ∈ ( 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ↦ ( 𝐻𝑥 ) ) )
12 offval3 ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → ( 𝐹f 𝑅 𝐺 ) = ( 𝑦 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹𝑦 ) 𝑅 ( 𝐺𝑦 ) ) ) )
13 12 adantr ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹𝐻 ) ∈ V ∧ ( 𝐺𝐻 ) ∈ V ) ) → ( 𝐹f 𝑅 𝐺 ) = ( 𝑦 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹𝑦 ) 𝑅 ( 𝐺𝑦 ) ) ) )
14 fveq2 ( 𝑦 = ( 𝐻𝑥 ) → ( 𝐹𝑦 ) = ( 𝐹 ‘ ( 𝐻𝑥 ) ) )
15 fveq2 ( 𝑦 = ( 𝐻𝑥 ) → ( 𝐺𝑦 ) = ( 𝐺 ‘ ( 𝐻𝑥 ) ) )
16 14 15 oveq12d ( 𝑦 = ( 𝐻𝑥 ) → ( ( 𝐹𝑦 ) 𝑅 ( 𝐺𝑦 ) ) = ( ( 𝐹 ‘ ( 𝐻𝑥 ) ) 𝑅 ( 𝐺 ‘ ( 𝐻𝑥 ) ) ) )
17 3 11 13 16 fmptco ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹𝐻 ) ∈ V ∧ ( 𝐺𝐻 ) ∈ V ) ) → ( ( 𝐹f 𝑅 𝐺 ) ∘ ( 𝐻 ↾ ( 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ) ) = ( 𝑥 ∈ ( 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ↦ ( ( 𝐹 ‘ ( 𝐻𝑥 ) ) 𝑅 ( 𝐺 ‘ ( 𝐻𝑥 ) ) ) ) )
18 ovex ( ( 𝐹𝑥 ) 𝑅 ( 𝐺𝑥 ) ) ∈ V
19 18 rgenw 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( ( 𝐹𝑥 ) 𝑅 ( 𝐺𝑥 ) ) ∈ V
20 eqid ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹𝑥 ) 𝑅 ( 𝐺𝑥 ) ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹𝑥 ) 𝑅 ( 𝐺𝑥 ) ) )
21 20 fnmpt ( ∀ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( ( 𝐹𝑥 ) 𝑅 ( 𝐺𝑥 ) ) ∈ V → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹𝑥 ) 𝑅 ( 𝐺𝑥 ) ) ) Fn ( dom 𝐹 ∩ dom 𝐺 ) )
22 19 21 mp1i ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹𝐻 ) ∈ V ∧ ( 𝐺𝐻 ) ∈ V ) ) → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹𝑥 ) 𝑅 ( 𝐺𝑥 ) ) ) Fn ( dom 𝐹 ∩ dom 𝐺 ) )
23 offval3 ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → ( 𝐹f 𝑅 𝐺 ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹𝑥 ) 𝑅 ( 𝐺𝑥 ) ) ) )
24 23 adantr ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹𝐻 ) ∈ V ∧ ( 𝐺𝐻 ) ∈ V ) ) → ( 𝐹f 𝑅 𝐺 ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹𝑥 ) 𝑅 ( 𝐺𝑥 ) ) ) )
25 24 fneq1d ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹𝐻 ) ∈ V ∧ ( 𝐺𝐻 ) ∈ V ) ) → ( ( 𝐹f 𝑅 𝐺 ) Fn ( dom 𝐹 ∩ dom 𝐺 ) ↔ ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹𝑥 ) 𝑅 ( 𝐺𝑥 ) ) ) Fn ( dom 𝐹 ∩ dom 𝐺 ) ) )
26 22 25 mpbird ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹𝐻 ) ∈ V ∧ ( 𝐺𝐻 ) ∈ V ) ) → ( 𝐹f 𝑅 𝐺 ) Fn ( dom 𝐹 ∩ dom 𝐺 ) )
27 26 fndmd ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹𝐻 ) ∈ V ∧ ( 𝐺𝐻 ) ∈ V ) ) → dom ( 𝐹f 𝑅 𝐺 ) = ( dom 𝐹 ∩ dom 𝐺 ) )
28 eqimss ( dom ( 𝐹f 𝑅 𝐺 ) = ( dom 𝐹 ∩ dom 𝐺 ) → dom ( 𝐹f 𝑅 𝐺 ) ⊆ ( dom 𝐹 ∩ dom 𝐺 ) )
29 cores2 ( dom ( 𝐹f 𝑅 𝐺 ) ⊆ ( dom 𝐹 ∩ dom 𝐺 ) → ( ( 𝐹f 𝑅 𝐺 ) ∘ ( 𝐻 ↾ ( dom 𝐹 ∩ dom 𝐺 ) ) ) = ( ( 𝐹f 𝑅 𝐺 ) ∘ 𝐻 ) )
30 27 28 29 3syl ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹𝐻 ) ∈ V ∧ ( 𝐺𝐻 ) ∈ V ) ) → ( ( 𝐹f 𝑅 𝐺 ) ∘ ( 𝐻 ↾ ( dom 𝐹 ∩ dom 𝐺 ) ) ) = ( ( 𝐹f 𝑅 𝐺 ) ∘ 𝐻 ) )
31 funcnvres2 ( Fun 𝐻 ( 𝐻 ↾ ( dom 𝐹 ∩ dom 𝐺 ) ) = ( 𝐻 ↾ ( 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ) )
32 1 31 syl ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹𝐻 ) ∈ V ∧ ( 𝐺𝐻 ) ∈ V ) ) → ( 𝐻 ↾ ( dom 𝐹 ∩ dom 𝐺 ) ) = ( 𝐻 ↾ ( 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ) )
33 32 coeq2d ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹𝐻 ) ∈ V ∧ ( 𝐺𝐻 ) ∈ V ) ) → ( ( 𝐹f 𝑅 𝐺 ) ∘ ( 𝐻 ↾ ( dom 𝐹 ∩ dom 𝐺 ) ) ) = ( ( 𝐹f 𝑅 𝐺 ) ∘ ( 𝐻 ↾ ( 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ) ) )
34 30 33 eqtr3d ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹𝐻 ) ∈ V ∧ ( 𝐺𝐻 ) ∈ V ) ) → ( ( 𝐹f 𝑅 𝐺 ) ∘ 𝐻 ) = ( ( 𝐹f 𝑅 𝐺 ) ∘ ( 𝐻 ↾ ( 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ) ) )
35 simpr2 ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹𝐻 ) ∈ V ∧ ( 𝐺𝐻 ) ∈ V ) ) → ( 𝐹𝐻 ) ∈ V )
36 simpr3 ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹𝐻 ) ∈ V ∧ ( 𝐺𝐻 ) ∈ V ) ) → ( 𝐺𝐻 ) ∈ V )
37 offval3 ( ( ( 𝐹𝐻 ) ∈ V ∧ ( 𝐺𝐻 ) ∈ V ) → ( ( 𝐹𝐻 ) ∘f 𝑅 ( 𝐺𝐻 ) ) = ( 𝑥 ∈ ( dom ( 𝐹𝐻 ) ∩ dom ( 𝐺𝐻 ) ) ↦ ( ( ( 𝐹𝐻 ) ‘ 𝑥 ) 𝑅 ( ( 𝐺𝐻 ) ‘ 𝑥 ) ) ) )
38 35 36 37 syl2anc ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹𝐻 ) ∈ V ∧ ( 𝐺𝐻 ) ∈ V ) ) → ( ( 𝐹𝐻 ) ∘f 𝑅 ( 𝐺𝐻 ) ) = ( 𝑥 ∈ ( dom ( 𝐹𝐻 ) ∩ dom ( 𝐺𝐻 ) ) ↦ ( ( ( 𝐹𝐻 ) ‘ 𝑥 ) 𝑅 ( ( 𝐺𝐻 ) ‘ 𝑥 ) ) ) )
39 dmco dom ( 𝐹𝐻 ) = ( 𝐻 “ dom 𝐹 )
40 dmco dom ( 𝐺𝐻 ) = ( 𝐻 “ dom 𝐺 )
41 39 40 ineq12i ( dom ( 𝐹𝐻 ) ∩ dom ( 𝐺𝐻 ) ) = ( ( 𝐻 “ dom 𝐹 ) ∩ ( 𝐻 “ dom 𝐺 ) )
42 inpreima ( Fun 𝐻 → ( 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) = ( ( 𝐻 “ dom 𝐹 ) ∩ ( 𝐻 “ dom 𝐺 ) ) )
43 1 42 syl ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹𝐻 ) ∈ V ∧ ( 𝐺𝐻 ) ∈ V ) ) → ( 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) = ( ( 𝐻 “ dom 𝐹 ) ∩ ( 𝐻 “ dom 𝐺 ) ) )
44 41 43 eqtr4id ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹𝐻 ) ∈ V ∧ ( 𝐺𝐻 ) ∈ V ) ) → ( dom ( 𝐹𝐻 ) ∩ dom ( 𝐺𝐻 ) ) = ( 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) )
45 simplr1 ( ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹𝐻 ) ∈ V ∧ ( 𝐺𝐻 ) ∈ V ) ) ∧ 𝑥 ∈ ( dom ( 𝐹𝐻 ) ∩ dom ( 𝐺𝐻 ) ) ) → Fun 𝐻 )
46 inss2 ( dom ( 𝐹𝐻 ) ∩ dom ( 𝐺𝐻 ) ) ⊆ dom ( 𝐺𝐻 )
47 dmcoss dom ( 𝐺𝐻 ) ⊆ dom 𝐻
48 46 47 sstri ( dom ( 𝐹𝐻 ) ∩ dom ( 𝐺𝐻 ) ) ⊆ dom 𝐻
49 48 a1i ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹𝐻 ) ∈ V ∧ ( 𝐺𝐻 ) ∈ V ) ) → ( dom ( 𝐹𝐻 ) ∩ dom ( 𝐺𝐻 ) ) ⊆ dom 𝐻 )
50 49 sselda ( ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹𝐻 ) ∈ V ∧ ( 𝐺𝐻 ) ∈ V ) ) ∧ 𝑥 ∈ ( dom ( 𝐹𝐻 ) ∩ dom ( 𝐺𝐻 ) ) ) → 𝑥 ∈ dom 𝐻 )
51 fvco ( ( Fun 𝐻𝑥 ∈ dom 𝐻 ) → ( ( 𝐹𝐻 ) ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐻𝑥 ) ) )
52 45 50 51 syl2anc ( ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹𝐻 ) ∈ V ∧ ( 𝐺𝐻 ) ∈ V ) ) ∧ 𝑥 ∈ ( dom ( 𝐹𝐻 ) ∩ dom ( 𝐺𝐻 ) ) ) → ( ( 𝐹𝐻 ) ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐻𝑥 ) ) )
53 inss1 ( dom ( 𝐹𝐻 ) ∩ dom ( 𝐺𝐻 ) ) ⊆ dom ( 𝐹𝐻 )
54 dmcoss dom ( 𝐹𝐻 ) ⊆ dom 𝐻
55 53 54 sstri ( dom ( 𝐹𝐻 ) ∩ dom ( 𝐺𝐻 ) ) ⊆ dom 𝐻
56 55 a1i ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹𝐻 ) ∈ V ∧ ( 𝐺𝐻 ) ∈ V ) ) → ( dom ( 𝐹𝐻 ) ∩ dom ( 𝐺𝐻 ) ) ⊆ dom 𝐻 )
57 56 sselda ( ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹𝐻 ) ∈ V ∧ ( 𝐺𝐻 ) ∈ V ) ) ∧ 𝑥 ∈ ( dom ( 𝐹𝐻 ) ∩ dom ( 𝐺𝐻 ) ) ) → 𝑥 ∈ dom 𝐻 )
58 fvco ( ( Fun 𝐻𝑥 ∈ dom 𝐻 ) → ( ( 𝐺𝐻 ) ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐻𝑥 ) ) )
59 45 57 58 syl2anc ( ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹𝐻 ) ∈ V ∧ ( 𝐺𝐻 ) ∈ V ) ) ∧ 𝑥 ∈ ( dom ( 𝐹𝐻 ) ∩ dom ( 𝐺𝐻 ) ) ) → ( ( 𝐺𝐻 ) ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐻𝑥 ) ) )
60 52 59 oveq12d ( ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹𝐻 ) ∈ V ∧ ( 𝐺𝐻 ) ∈ V ) ) ∧ 𝑥 ∈ ( dom ( 𝐹𝐻 ) ∩ dom ( 𝐺𝐻 ) ) ) → ( ( ( 𝐹𝐻 ) ‘ 𝑥 ) 𝑅 ( ( 𝐺𝐻 ) ‘ 𝑥 ) ) = ( ( 𝐹 ‘ ( 𝐻𝑥 ) ) 𝑅 ( 𝐺 ‘ ( 𝐻𝑥 ) ) ) )
61 44 60 mpteq12dva ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹𝐻 ) ∈ V ∧ ( 𝐺𝐻 ) ∈ V ) ) → ( 𝑥 ∈ ( dom ( 𝐹𝐻 ) ∩ dom ( 𝐺𝐻 ) ) ↦ ( ( ( 𝐹𝐻 ) ‘ 𝑥 ) 𝑅 ( ( 𝐺𝐻 ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ↦ ( ( 𝐹 ‘ ( 𝐻𝑥 ) ) 𝑅 ( 𝐺 ‘ ( 𝐻𝑥 ) ) ) ) )
62 38 61 eqtrd ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹𝐻 ) ∈ V ∧ ( 𝐺𝐻 ) ∈ V ) ) → ( ( 𝐹𝐻 ) ∘f 𝑅 ( 𝐺𝐻 ) ) = ( 𝑥 ∈ ( 𝐻 “ ( dom 𝐹 ∩ dom 𝐺 ) ) ↦ ( ( 𝐹 ‘ ( 𝐻𝑥 ) ) 𝑅 ( 𝐺 ‘ ( 𝐻𝑥 ) ) ) ) )
63 17 34 62 3eqtr4d ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun 𝐻 ∧ ( 𝐹𝐻 ) ∈ V ∧ ( 𝐺𝐻 ) ∈ V ) ) → ( ( 𝐹f 𝑅 𝐺 ) ∘ 𝐻 ) = ( ( 𝐹𝐻 ) ∘f 𝑅 ( 𝐺𝐻 ) ) )