theorem Th5: :: WAYBEL29:5

for S1, S2, T1, T2 being RelStr st RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) holds
for f being Function of S1,T1 st f is isomorphic holds
for g being Function of S2,T2 st g = f holds
g is isomorphic