theorem Th54: :: FUNCT_3:54

for f, g, h, k being Function st dom f = dom g & dom k = dom h & <:f,g:> = <:k,h:> holds
( f = k & g = h )