lemma

draft/draft.tex

@@ -2489,9 +2489,26 @@ Now, we make the proof more abstract. We prove the statement for set-functors of
 	For sets $X$ and $Y$ in $\powf A$, and a function $f\c A\to B$ the following equation holds:
 	\begin{gather*}
 		%(\powf p_i)^\dagger(R_1\cup R_2)=(\powf p_i)^\dagger(R_1)\cup(\powf p_i)^\dagger(R_2)
-		\powf f(X\cup Y)=\powf f(X)\cup(\powf f)(Y)
+		\powf f(X\cup Y)=\powf f(X)\cup \powf f(Y)
 	\end{gather*}
 \end{lemma}
+\begin{proof}
+	Assuming $b\in\powf f(X_1\cup X_2)$ then exists $z$ that $z\in X_1\cup X_2$ and $f(z)=b$, thus either $z\in X_1$ or $z\in X_2$, so we have $b\in\powf f(X_1)$ or $b\in\powf f(X_2)$, respectively. So, we have $b\in \powf f(X_1)\cup\powf f(X_2)$.
+	
+	Now, assuming that $b\in\powf f(X_1)\cup\powf f(X_2)$ then we either have $b\in\powf f(X_1)$ or $b\in\powf f(X_2)$. Without loss of generality, we assume $b\in\powf f(X_j)$, where $j\in\{1,2\}$.	
+	Then there exists $z$ that $z\in X_j$ and $f(z)=b$, so we have $z\in X_1\cup X_2$ that gives $b\in\powf f(X_1\cup X_2)$.\qed
+	%	We prove the lemma for the case that $i=1$. The proof is the same for $i=2$.
+	%	
+	%	First, we prove $(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)\subseteq(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s\join(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$.
+	%	Assuming $y_1\in(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$ then exists $y_2$ that we have either $(y_1,y_2)\in(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$ or $(y_1,y_2)\in\sigma(x_1,x_2)$. So, we have either $y_1\in(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$ or $y_1\in(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$ that means that we have $y_1\in(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s\join(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$.
+	%	
+	%	Now, we prove $(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s\join(\powf p_1)^\dagger\comp\sigma(x_1,x_2)\subseteq(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$. Assuming $y_1\in(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s\join(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$ then we have:
+	%	\begin{itemize}
+		%		\item $y_1\in(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$: Then there exists $y_2$ such that $(y_1,y_2)\in(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$. So, $(y_1,y_2)\in(\powf s)^\dagger\comp\sigma\comp s\join\sigma(x_1,x_2)$, thus $y_1\in(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$.
+		%		\item $y_1\in(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$: Then there exists $y_2$ such that $(y_1,y_2)\in\sigma(x_1,x_2)$. So, $(y_1,y_2)\in(\powf s)^\dagger\comp\sigma\comp s\join\sigma(x_1,x_2)$, thus $y_1\in(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$.
+		%	\end{itemize} \qed
+	%	\todo{Rewrite the proof according to the statement!}
+\end{proof}
 \todo{Finish this proof. With this, you can give the proof for $\powf F$. After you finished this, you can remove the previous sections.}
 
 \subsection{Maybe Functor}