let x, y, z be set ; :: thesis: ( z in x U+ y implies ( z = [(z `1),(z `2)] & ( ( z `2 = 1 & z `1 in x ) or ( z `2 = 2 & z `1 in y ) ) ) )
assume z in x U+ y ; :: thesis: ( z = [(z `1),(z `2)] & ( ( z `2 = 1 & z `1 in x ) or ( z `2 = 2 & z `1 in y ) ) )
then z in [:x,{1}:] \/ [:y,{2}:] by Th73;
then ( z in [:x,{1}:] or z in [:y,{2}:] ) by XBOOLE_0:def 3;
hence ( z = [(z `1),(z `2)] & ( ( z `2 = 1 & z `1 in x ) or ( z `2 = 2 & z `1 in y ) ) ) by MCART_1:13, MCART_1:21; :: thesis: verum