Identity up to isomorphism treated as identity in proof

The proof is indeed worded poorly wrt $varphi'(0,0)$. It is also not necessary to do the identification $E=F_1$; the complication you get from considering them to be different is very manageable. Additionally using the word toplinear is a crime. Let me rewrite the proof with your two questions in mind:

Define $$varphi: Utimes F_2to F_1times F_2, qquad (x,y)mapsto f(x)+(0,y)$$ Then the derivative of $varphi$ at $(x_0,0)$ is equal to $f'(x_0)+(0,mathrm{id}_{F_2})$. Since $f'(x_0)$ is valued in $F_1$ and is a linear isomorphism you have that $varphi'(x_0,0)$ is also a linear isomorphism.

By the inverse function theorem it follows that there is a neighbourhood $Vsubseteq Utimes F_2$ of $(x_0,0)$ so that $varphilvert_V$ is a diffeomorphism (understood to imply $p$-times differentiable). Let $h$ denote the inverse of $varphilvert_V$ and define $g:=(f'(x_0),mathrm{id}_{F_2})circ h$. As a composition of diffeomorphisms $g$ is a diffeomorphism. Let $U_1$ be the projection of $V$ onto the $E$ component.

Then for $xin U_1$: $$g(f(x)) = (f'(x_0), mathrm{id}_{F_2})left[h(varphi(x,0))right]= (f'(x_0),mathrm{id}_{F_2}) [(x,0)] = (f'(x_0)[x],0)$$ and $gcirc f$ is valued in $F_1times{0}subseteq F_1times F_2$.