theorem Th19: :: WAYBEL24:19

for S being set
for T being non empty RelStr
for f being set holds
( f is Element of (T |^ S) iff f is Function of S, the carrier of T )