let x, y, z, t be object ; :: thesis: ( proj1 {[x,y],[z,t]} = {x,z} & proj2 {[x,y],[z,t]} = {y,t} )
A1: ( proj2 {[x,y]} = {y} & proj2 {[z,t]} = {t} ) by Th6;
{[x,y],[z,t]} = {[x,y]} \/ {[z,t]} by ENUMSET1:1;
then A2: ( proj1 {[x,y],[z,t]} = (proj1 {[x,y]}) \/ (proj1 {[z,t]}) & proj2 {[x,y],[z,t]} = (proj2 {[x,y]}) \/ (proj2 {[z,t]}) ) by XTUPLE_0:23, XTUPLE_0:27;
( proj1 {[x,y]} = {x} & proj1 {[z,t]} = {z} ) by Th6;
hence ( proj1 {[x,y],[z,t]} = {x,z} & proj2 {[x,y],[z,t]} = {y,t} ) by A2, A1, ENUMSET1:1; :: thesis: verum