per cases ( X = {} or Y = {} or ( X <> {} & Y <> {} ) ) ;

suppose A1: ( X = {} or Y = {} ) ; :: thesis: UNION (X,Y) is finite

UNION (X,Y) = {}

proof

assume UNION (X,Y) <> {} ; :: thesis: contradiction
then consider xy being object such that
A2: xy in UNION (X,Y) by XBOOLE_0:def 1;
ex x, y being set st
( x in X & y in Y & xy = x \/ y ) by A2, SETFAM_1:def 4;
hence contradiction by A1; :: thesis: verum

end;

hence UNION (X,Y) is finite ; :: thesis: verum

end;

suppose ( X <> {} & Y <> {} ) ; :: thesis: UNION (X,Y) is finite

then reconsider X = X, Y = Y as non empty finite set ;
deffunc H₁( set , set ) -> set = X \/ Y;
set XY = { H₁(u,v) where u is Element of X, v is Element of Y : ( u in X & v in Y ) } ;
A3: UNION (X,Y) c= { H₁(u,v) where u is Element of X, v is Element of Y : ( u in X & v in Y ) }

proof

let xy be object ; :: according to TARSKI:def 3 :: thesis: ( not xy in UNION (X,Y) or xy in { H₁(u,v) where u is Element of X, v is Element of Y : ( u in X & v in Y ) } )
assume xy in UNION (X,Y) ; :: thesis: xy in { H₁(u,v) where u is Element of X, v is Element of Y : ( u in X & v in Y ) }
then ex x, y being set st
( x in X & y in Y & xy = x \/ y ) by SETFAM_1:def 4;
hence xy in { H₁(u,v) where u is Element of X, v is Element of Y : ( u in X & v in Y ) } ; :: thesis: verum

end;

A4: X is finite ;
A5: Y is finite ;
{ H₁(u,v) where u is Element of X, v is Element of Y : ( u in X & v in Y ) } is finite from FRAENKEL:sch 22(A4, A5);
hence UNION (X,Y) is finite by A3; :: thesis: verum

end;

end;