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 H1( Ordinal) -> set = p . $1;
deffunc H2( Ordinal) -> set = q . ($1 -^ domp);
defpred S1[ 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
( ( S1[x] implies f . x = H1(x) ) & ( not S1[x] implies f . x = H2(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;
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