Finite-support products of Knaster posets are Knaster

Well-order $X$ using F5 and A1 and take an injective family $(p_{\xi }{)}_{\xi <{\omega }_1}$ from it, possible since $X$ is uncountable. By F3 the supports $a_{\xi }$ are finite. Apply F1 to obtain an uncountable $J\subseteq {\omega }_1$ and finite $r$ with $a_{\xi }\cap a_{\eta }=r$ for distinct $\xi ,\eta \in J$. In particular $r\subseteq a_{\xi }$ for every $\xi \in J$, since each index has a distinct partner in $J$.

Each restriction $p_{\xi }\upharpoonright r$ belongs to the finite product ${\prod }_{i\in r}{P}_i$. Enumerate the finite set $r$ to apply F2 and obtain uncountable $K\subseteq J$ with pairwise compatible restrictions. Repeated restrictions cause no loss of indices because F2 states its indexed version. If $r=\mathrm{\varnothing }$, all restrictions are the empty tuple and one may take $K=J$.

Fix distinct $\xi ,\eta \in K$. On $r$ take a tuple $q$ below both restrictions. On $a_{\xi }\setminus r$ use $p_{\xi }(i)$, and on $a_{\eta }\setminus r$ use $p_{\eta }(i)$. These two sets are disjoint by step 1.1. Put $s(i)=1_i$ outside $a_{\xi }\cup a_{\eta }$. On a petal the other condition has value $1_i$, so the chosen value is below both; on $r$ use $q$; elsewhere both original values are $1_i$. Thus $s\le p_{\xi },p_{\eta }$ and its support is contained in the finite union $a_{\xi }\cup a_{\eta }$, so F3 puts $s$ in the product. The family $(p_{\xi }{)}_{\xi \in K}$ remains injective, giving an uncountable compatible subset of $X$. Hence the product is Knaster and is ccc by F4.

For the partial-function assertion, take a disjoint tagged copy $\widehat{C}$ of $C$ and a new element $\mathrm{\top }$. Let $Q=\widehat{C}\cup \{\mathrm{\top }\}$, with $u\le v$ iff $u=v$ or $v=\mathrm{\top }$. This is a partial order: reflexivity holds by equality, distinct tagged values are unrelated, and any strict comparison ends at $\mathrm{\top }$, which verifies antisymmetry and transitivity. It is countable and has greatest element $\mathrm{\top }$, so F4 makes it Knaster. A finite partial function $f$ corresponds to the tuple equal to the tagged $f(i)$ on its domain and $\mathrm{\top }$ elsewhere. The support is exactly $\mathrm{dom}(f)$; conversely any finite-support tuple gives exactly that finite partial function. Moreover, the tuple of $g$ is below that of $f$ precisely when $g$ extends $f$, because a tagged value has no smaller element other than itself. This order isomorphism transfers the Knaster conclusion of step 3.1 to finite partial functions. The empty domain maps to the greatest tuple, and for $I=\mathrm{\varnothing }$ both posets are singletons.