Metamath Proof Explorer


Theorem hocoi

Description: Composition of Hilbert space operators. (Contributed by NM, 12-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypotheses hoeq.1 S:
hoeq.2 T:
Assertion hocoi ASTA=STA

Proof

Step Hyp Ref Expression
1 hoeq.1 S:
2 hoeq.2 T:
3 fvco3 T:ASTA=STA
4 2 3 mpan ASTA=STA