let x, y be set ; :: thesis: 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 :: thesis: for z being object holds
( z in x U+ y iff z in [:x,{1}:] \/ [:y,{2}:] )

let z be object ; :: thesis: ( 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, XBOOLE_0:def 3; :: thesis: verum

end;

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