theorem :: FUNCT_5:13

for x, y, z, t being object holds
( proj1 {[x,y],[z,t]} = {x,z} & proj2 {[x,y],[z,t]} = {y,t} )