theorem :: FUNCT_4:131

for a, b, x, y, z being object holds (a,a,b) --> (x,y,z) = (a,b) --> (y,z) by Th81;