theorem Th11: :: TOPS_5:11

for f being Function
for i, j being object st i in dom f & j in dom f holds
f = f +* ((i,j) --> ((f . i),(f . j)))