let x, y be set ; x U+ y = [:x,{1}:] \/ [:y,{2}:]
len <*x,y*> = 2
by FINSEQ_1:44;
then A1:
dom <*x,y*> = {1,2}
by FINSEQ_1:2, FINSEQ_1:def 3;
now for z being object holds
( z in x U+ y iff z in [:x,{1}:] \/ [:y,{2}:] )let z be
object ;
( z in x U+ y iff z in [:x,{1}:] \/ [:y,{2}:] )A2:
(
z `2 in {1,2} iff (
z `2 = 1 or
z `2 = 2 ) )
by TARSKI:def 2;
A3:
(
z in [:x,{1}:] iff (
z `1 in x &
z `2 = 1 &
z = [(z `1),(z `2)] ) )
by MCART_1:13, MCART_1:21, ZFMISC_1:106;
A4:
(
z in [:y,{2}:] iff (
z `1 in y &
z `2 = 2 &
z = [(z `1),(z `2)] ) )
by MCART_1:13, MCART_1:21, ZFMISC_1:106;
(
z in x U+ y iff (
z `2 in {1,2} &
z `1 in <*x,y*> . (z `2) &
z = [(z `1),(z `2)] ) )
by A1, CARD_3:22;
hence
(
z in x U+ y iff
z in [:x,{1}:] \/ [:y,{2}:] )
by A2, A3, A4, FINSEQ_1:44, XBOOLE_0:def 3;
verum end;
hence
x U+ y = [:x,{1}:] \/ [:y,{2}:]
by TARSKI:2; verum