let X, Y, Z, y be set ; :: thesis: ( y <> {} & y c= Y implies [:X,y:] * [:Y,Z:] = [:X,Z:] )
assume y <> {} ; :: thesis: ( not y c= Y or [:X,y:] * [:Y,Z:] = [:X,Z:] )
then reconsider yy = y as non empty set ;
set P = [:X,yy:];
set Q = [:Y,Z:];
assume y c= Y ; :: thesis: [:X,y:] * [:Y,Z:] = [:X,Z:]
then reconsider z = rng [:X,yy:] as Subset of Y by XBOOLE_1:1;
( ([:X,yy:] " (Y \/ z)) \+\ (dom [:X,yy:]) = {} & (dom [:X,yy:]) \+\ X = {} ) ;
then ( [:X,yy:] " Y = dom [:X,yy:] & dom [:X,yy:] = X ) by Th29;
hence [:X,y:] * [:Y,Z:] = [:X,Z:] by Lm61; :: thesis: verum