let A, B be set ; :: thesis: (Fin A) \/ (Fin B) c= Fin (A \/ B)
( Fin A c= Fin (A \/ B) & Fin B c= Fin (A \/ B) ) by Th10, XBOOLE_1:7;
hence (Fin A) \/ (Fin B) c= Fin (A \/ B) by XBOOLE_1:8; :: thesis: verum