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 Th74;
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:23; :: thesis: verum