[proofplan] We construct the two maps fibre by fibre using the defining description of the pullback bundle. For direct sums, the map separates a vector $e \oplus u$ over $f(x)$ into its two pulled-back components over $x$, and the inverse recombines them. For tensor products, the universal bilinear construction gives a fibrewise [linear map](/page/Linear%20Map) on each [tensor product](/page/Tensor%20Product), and the inverse is obtained by forgetting the pullback labels. Smoothness is checked in local frames, where both maps become the identity linear identification on coordinate vector spaces. [/proofplan]

[step:Define the direct-sum map and its inverse on fibres] Let \begin{align*} \Pi_\oplus: f^*(E \oplus F) &\to f^*E \oplus f^*F \end{align*} be the map over $M$ defined as follows. For $x \in M$, $e \in E_{f(x)}$, and $u \in F_{f(x)}$, set \begin{align*} \Pi_\oplus(x, e \oplus u) := (x,e) \oplus (x,u). \end{align*} This is well-defined because $e$ and $u$ lie in the same fibre over $f(x)$, so $(x,e) \in (f^*E)_x$ and $(x,u) \in (f^*F)_x$. Define \begin{align*} \Psi_\oplus: f^*E \oplus f^*F &\to f^*(E \oplus F) \end{align*} by \begin{align*} \Psi_\oplus\bigl((x,e) \oplus (x,u)\bigr) := (x, e \oplus u), \end{align*} for $x \in M$, $e \in E_{f(x)}$, and $u \in F_{f(x)}$. The same fibre condition shows that this is well-defined. For every $x \in M$, the restriction \begin{align*} (\Pi_\oplus)_x: (E \oplus F)_{f(x)} \to E_{f(x)} \oplus F_{f(x)} \end{align*} is the linear map determined by \begin{align*} (\Pi_\oplus)_x(e \oplus u) = e \oplus u. \end{align*} The restriction \begin{align*} (\Psi_\oplus)_x: E_{f(x)} \oplus F_{f(x)} \to (E \oplus F)_{f(x)} \end{align*} is the linear map determined by \begin{align*} (\Psi_\oplus)_x(e \oplus u) = e \oplus u. \end{align*} These two linear maps are inverse to each other. Hence $\Pi_\oplus$ is a fibrewise linear bijection with inverse $\Psi_\oplus$. [/step]

[step:Define the tensor-product map and its inverse on fibres]For each $x \in M$, define the map \begin{align*} \beta_x: E_{f(x)} \times F_{f(x)} \to (f^*E)_x \otimes (f^*F)_x \end{align*} by \begin{align*} \beta_x(e,u) = (x,e) \otimes (x,u). \end{align*} This map is bilinear because the pullback fibre operations are inherited from the [vector space](/page/Vector%20Space) operations on $E_{f(x)}$ and $F_{f(x)}$. By the defining [universal property of the tensor product](/theorems/3971), there is a unique linear map \begin{align*} (\Pi_\otimes)_x: E_{f(x)} \otimes F_{f(x)} &\to (f^*E)_x \otimes (f^*F)_x \end{align*} such that \begin{align*} (\Pi_\otimes)_x(e \otimes u) = (x,e) \otimes (x,u) \end{align*} for all $e \in E_{f(x)}$ and $u \in F_{f(x)}$. Define the total map \begin{align*} \Pi_\otimes: f^*(E \otimes F) &\to f^*E \otimes f^*F \end{align*} by \begin{align*} \Pi_\otimes(x,w) := \bigl(x,(\Pi_\otimes)_x(w)\bigr), \end{align*} where $x \in M$ and $w \in (E \otimes F)_{f(x)}$. Similarly, for each $x \in M$, define the map \begin{align*} \gamma_x: (f^*E)_x \times (f^*F)_x \to E_{f(x)} \otimes F_{f(x)} \end{align*} by \begin{align*} \gamma_x\bigl((x,e),(x,u)\bigr) = e \otimes u. \end{align*} This map is bilinear because addition and scalar multiplication in $(f^*E)_x$ and $(f^*F)_x$ are defined through the fibres $E_{f(x)}$ and $F_{f(x)}$. Therefore it induces a unique linear map \begin{align*} (\Psi_\otimes)_x: (f^*E)_x \otimes (f^*F)_x &\to E_{f(x)} \otimes F_{f(x)} \end{align*} with \begin{align*} (\Psi_\otimes)_x\bigl((x,e) \otimes (x,u)\bigr) = e \otimes u. \end{align*} Thus define \begin{align*} \Psi_\otimes: f^*E \otimes f^*F &\to f^*(E \otimes F) \end{align*} by \begin{align*} \Psi_\otimes(x,z) := \bigl(x,(\Psi_\otimes)_x(z)\bigr), \end{align*} where $x \in M$ and $z \in (f^*E)_x \otimes (f^*F)_x$. On pure tensors, the composites satisfy \begin{align*} (\Psi_\otimes)_x(\Pi_\otimes)_x(e \otimes u) = e \otimes u \end{align*} and \begin{align*} (\Pi_\otimes)_x(\Psi_\otimes)_x\bigl((x,e) \otimes (x,u)\bigr) = (x,e) \otimes (x,u). \end{align*} Since pure tensors span the corresponding tensor products, the two composites are identity maps. Hence $\Pi_\otimes$ is a fibrewise linear bijection with inverse $\Psi_\otimes$.[/step]

[guided]Fix $x \in M$. The tensor case needs one extra layer of care because an element of $E_{f(x)} \otimes F_{f(x)}$ is generally a finite sum of pure tensors, not a single pure tensor. We therefore first define the map on pairs and then use the tensor product property to extend it linearly. Define \begin{align*} \beta_x: E_{f(x)} \times F_{f(x)} \to (f^*E)_x \otimes (f^*F)_x \end{align*} by \begin{align*} \beta_x(e,u) = (x,e) \otimes (x,u). \end{align*} This map is bilinear because addition and scalar multiplication in the pullback fibres are inherited from the original fibres $E_{f(x)}$ and $F_{f(x)}$. Hence the universal property of the tensor product gives a unique linear map \begin{align*} (\Pi_\otimes)_x: E_{f(x)} \otimes F_{f(x)} &\to (f^*E)_x \otimes (f^*F)_x \end{align*} satisfying \begin{align*} (\Pi_\otimes)_x(e \otimes u) = (x,e) \otimes (x,u). \end{align*} This is exactly the announced fibre formula, now interpreted correctly as a linear map on the whole tensor product. To construct the inverse, define \begin{align*} \gamma_x: (f^*E)_x \times (f^*F)_x \to E_{f(x)} \otimes F_{f(x)} \end{align*} by \begin{align*} \gamma_x\bigl((x,e),(x,u)\bigr) = e \otimes u. \end{align*} Again this is bilinear, so it induces a unique linear map \begin{align*} (\Psi_\otimes)_x: (f^*E)_x \otimes (f^*F)_x &\to E_{f(x)} \otimes F_{f(x)} \end{align*} such that \begin{align*} (\Psi_\otimes)_x\bigl((x,e) \otimes (x,u)\bigr) = e \otimes u. \end{align*} These fibrewise maps assemble into total maps over $M$: define \begin{align*} \Pi_\otimes: f^*(E \otimes F) \to f^*E \otimes f^*F \end{align*} by \begin{align*} \Pi_\otimes(x,w) = \bigl(x,(\Pi_\otimes)_x(w)\bigr), \end{align*} where $x \in M$ and $w \in (E \otimes F)_{f(x)}$. Define \begin{align*} \Psi_\otimes: f^*E \otimes f^*F \to f^*(E \otimes F) \end{align*} by \begin{align*} \Psi_\otimes(x,z) = \bigl(x,(\Psi_\otimes)_x(z)\bigr), \end{align*} where $x \in M$ and $z \in (f^*E)_x \otimes (f^*F)_x$. Now check the composites. For every pure tensor $e \otimes u \in E_{f(x)} \otimes F_{f(x)}$, \begin{align*} (\Psi_\otimes)_x(\Pi_\otimes)_x(e \otimes u) = (\Psi_\otimes)_x\bigl((x,e) \otimes (x,u)\bigr) = e \otimes u. \end{align*} Since pure tensors span $E_{f(x)} \otimes F_{f(x)}$, this proves \begin{align*} (\Psi_\otimes)_x \circ (\Pi_\otimes)_x = \operatorname{id}_{E_{f(x)} \otimes F_{f(x)}}. \end{align*} Similarly, for every pure tensor $(x,e) \otimes (x,u) \in (f^*E)_x \otimes (f^*F)_x$, \begin{align*} (\Pi_\otimes)_x(\Psi_\otimes)_x\bigl((x,e) \otimes (x,u)\bigr) = (\Pi_\otimes)_x(e \otimes u) = (x,e) \otimes (x,u). \end{align*} Since such pure tensors span $(f^*E)_x \otimes (f^*F)_x$, we also have \begin{align*} (\Pi_\otimes)_x \circ (\Psi_\otimes)_x = \operatorname{id}_{(f^*E)_x \otimes (f^*F)_x}. \end{align*} Thus the tensor map is a fibrewise linear isomorphism, with inverse obtained by forgetting the pullback label $x$ inside each pulled-back factor.[/guided]

[step:Check smoothness in local frames] Let $x_0 \in M$ and set $y_0 := f(x_0) \in N$. Choose an open neighbourhood $V \subset N$ of $y_0$ over which both $E$ and $F$ are trivial. Let $r$ be the rank of $E$ and $s$ the rank of $F$. Choose smooth local frames $e_1,\dots,e_r: V \to E$ and $u_1,\dots,u_s: V \to F$. Set $U := f^{-1}(V) \subset M$. The pullback frames over $U$ are the smooth sections \begin{align*} \widetilde e_i: U &\to f^*E, & x &\mapsto (x,e_i(f(x))), \end{align*} for $1 \le i \le r$, and \begin{align*} \widetilde u_a: U &\to f^*F, & x &\mapsto (x,u_a(f(x))), \end{align*} for $1 \le a \le s$. For direct sums, the frame of $f^*(E \oplus F)$ over $U$ obtained from \begin{align*} e_1 \oplus 0,\dots,e_r \oplus 0,0 \oplus u_1,\dots,0 \oplus u_s \end{align*} is carried by $\Pi_\oplus$ to the frame \begin{align*} \widetilde e_1 \oplus 0,\dots,\widetilde e_r \oplus 0,0 \oplus \widetilde u_1,\dots,0 \oplus \widetilde u_s \end{align*} of $f^*E \oplus f^*F$. Therefore the coordinate representative of $\Pi_\oplus$ over $U$ is the identity linear map on $\mathbb{R}^{r+s}$. For tensor products, the frame of $f^*(E \otimes F)$ over $U$ obtained from \begin{align*} e_i \otimes u_a \end{align*} for $1 \le i \le r$ and $1 \le a \le s$ is carried by $\Pi_\otimes$ to the frame \begin{align*} \widetilde e_i \otimes \widetilde u_a \end{align*} of $f^*E \otimes f^*F$. Therefore the coordinate representative of $\Pi_\otimes$ over $U$ is the identity linear map on $\mathbb{R}^{rs}$. The coordinate representative of $\Psi_\oplus$ over $U$ sends the ordered frame \begin{align*} \widetilde e_1 \oplus 0,\dots,\widetilde e_r \oplus 0,0 \oplus \widetilde u_1,\dots,0 \oplus \widetilde u_s \end{align*} of $f^*E \oplus f^*F$ back to the ordered pullback frame of $f^*(E \oplus F)$ obtained from \begin{align*} e_1 \oplus 0,\dots,e_r \oplus 0,0 \oplus u_1,\dots,0 \oplus u_s, \end{align*} so it is the identity linear map on $\mathbb{R}^{r+s}$. The coordinate representative of $\Psi_\otimes$ over $U$ sends the frame \begin{align*} \widetilde e_i \otimes \widetilde u_a \end{align*} of $f^*E \otimes f^*F$ back to the pullback frame of $f^*(E \otimes F)$ obtained from \begin{align*} e_i \otimes u_a, \end{align*} for $1 \le i \le r$ and $1 \le a \le s$, so it is the identity linear map on $\mathbb{R}^{rs}$. These four identity coordinate representatives are smooth. Since smoothness of a vector bundle map is local in bundle trivializations, all four maps are smooth. [/step]

[step:Conclude that the fibrewise maps are canonical vector bundle isomorphisms] The maps $\Pi_\oplus$ and $\Pi_\otimes$ cover the identity map $\operatorname{id}_M: M \to M$ because each sends a vector over $x \in M$ to a vector over the same point $x$. The preceding steps show that each map is smooth, fibrewise linear, and has a smooth fibrewise linear inverse. Hence $\Pi_\oplus$ is a smooth vector bundle isomorphism \begin{align*} f^*(E \oplus F) \cong f^*E \oplus f^*F, \end{align*} and $\Pi_\otimes$ is a smooth vector bundle isomorphism \begin{align*} f^*(E \otimes F) \cong f^*E \otimes f^*F. \end{align*} Their formulas use only the defining fibres of pullback, direct sum, and tensor product, and therefore do not depend on any chosen trivialization or local frame. This proves the stated canonical identifications. [/step]