let x, y be set ; :: thesis: x U+ y = [:x,{1}:] \/ [:y,{2}:]
len <*x,y*> = 2 by FINSEQ_1:61;
then A1: dom <*x,y*> = {1,2} by FINSEQ_1:4, FINSEQ_1:def 3;

now

let z be set ; :: thesis: ( z in x U+ y iff z in [:x,{1}:] \/ [:y,{2}:] )
A2: ( 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:33;
A3: ( z `2 in {1,2} iff ( z `2 = 1 or z `2 = 2 ) ) by TARSKI:def 2;
A4: ( z in [:x,{1}:] iff ( z `1 in x & z `2 = 1 & z = [(z `1 ),(z `2 )] ) ) by MCART_1:13, MCART_1:23, ZFMISC_1:129;
( z in [:y,{2}:] iff ( z `1 in y & z `2 = 2 & z = [(z `1 ),(z `2 )] ) ) by MCART_1:13, MCART_1:23, ZFMISC_1:129;
hence ( z in x U+ y iff z in [:x,{1}:] \/ [:y,{2}:] ) by A2, A3, A4, FINSEQ_1:61, XBOOLE_0:def 3; :: thesis: verum

end;

hence x U+ y = [:x,{1}:] \/ [:y,{2}:] by TARSKI:2; :: thesis: verum