theorem Th5: :: ALGSPEC1:5

for X1, Y1, X2, Y2 being non empty set
for f being Function of X1,X2
for g being Function of Y1,Y2 st f c= g holds
f * c= g *