let A, B be set ; :: thesis: ( A is finite & B is finite implies A \/ B is finite )
given p being Function such that A1: rng p = A and
A2: dom p in omega ; :: according to FINSET_1:def 1 :: thesis: ( not B is finite or A \/ B is finite )
given q being Function such that A3: rng q = B and
A4: dom q in omega ; :: according to FINSET_1:def 1 :: thesis: A \/ B is finite
reconsider domp = dom p, domq = dom q as Ordinal by A2, A4;
deffunc H₁( Ordinal) -> set = p . $1;
deffunc H₂( Ordinal) -> set = q . ($1 -^ domp);
defpred S₁[ set ] means $1 in domp;
consider f being Function such that
A5: dom f = domp +^ domq and
A6: for x being Ordinal st x in domp +^ domq holds
( ( S₁[x] implies f . x = H₁(x) ) & ( not S₁[x] implies f . x = H₂(x) ) ) from FINSET_1:sch 1();
take f ; :: according to FINSET_1:def 1 :: thesis: ( rng f = A \/ B & dom f in omega )
reconsider domp = domp, domq = domq as natural Ordinal by A2, A4;
thus rng f = A \/ B :: thesis: dom f in omega

proof

thus rng f c= A \/ B :: according to XBOOLE_0:def 10 :: thesis: A \/ B c= rng f

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in A \/ B )
assume y in rng f ; :: thesis: y in A \/ B
then consider x being object such that
A7: x in dom f and
A8: y = f . x by FUNCT_1:def 3;
reconsider x = x as Ordinal by A5, A7;

per cases ( x in domp or not x in domp ) ;

suppose A9: x in domp ; :: thesis: y in A \/ B

then A10: y = p . x by A5, A6, A7, A8;
p . x in rng p by A9, FUNCT_1:def 3;
hence y in A \/ B by A1, A10, XBOOLE_0:def 3; :: thesis: verum

end;

suppose A11: not x in domp ; :: thesis: y in A \/ B

then A12: domp c= x by ORDINAL1:16;
A13: y = q . (x -^ domp) by A5, A6, A7, A8, A11;
domp +^ (x -^ domp) = x by A12, ORDINAL3:def 5;
then x -^ domp in dom q by A5, A7, ORDINAL3:22;
then y in B by A3, A13, FUNCT_1:def 3;
hence y in A \/ B by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A \/ B or x in rng f )
assume A14: x in A \/ B ; :: thesis: x in rng f

per cases ( x in rng p or x in rng q ) by A1, A3, A14, XBOOLE_0:def 3;

suppose x in rng p ; :: thesis: x in rng f

then consider y being object such that
A15: y in dom p and
A16: x = p . y by FUNCT_1:def 3;
A17: dom p c= dom f by A5, ORDINAL3:24;
then x = f . y by A5, A6, A15, A16;
hence x in rng f by A15, A17, FUNCT_1:def 3; :: thesis: verum

end;

suppose x in rng q ; :: thesis: x in rng f

then consider y being object such that
A18: y in domq and
A19: x = q . y by FUNCT_1:def 3;
reconsider y = y as Ordinal by A18;
set z = domp +^ y;
domp c= domp +^ y by ORDINAL3:24;
then A20: not domp +^ y in domp by ORDINAL1:5;
A21: domp +^ y in dom f by A5, A18, ORDINAL3:17;
x = q . ((domp +^ y) -^ domp) by A19, ORDINAL3:52
.= f . (domp +^ y) by A5, A6, A20, A21 ;
hence x in rng f by A21, FUNCT_1:def 3; :: thesis: verum

end;

end;

end;

domp +^ domq is natural ;
hence dom f in omega by A5; :: thesis: verum